OCamlでlet recを使わずにfact関数を定義する - にわとり小屋でのプログラミング
今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。 Inductive t (A: Set) : Set := | T : (t A -> A) -> t A. 一見なんの問題も無さそうな この型定義は失敗し、次のようなコンパイルエラーが出力される。 Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".もしこの型が定義できたとすると次のような関数が定義できてしまう。 Definition ワォ (T f) := f (T f). ここで (ワォ (T ワォ)
λx.x K S K ＠ はてな - #009 賢人鳥をまねる
OCaml では，let rec を使わずに再帰関数を模倣することができる． 但し「for ループを使えばできる」とかそういう話ではない． 例えば，階乗を計算する関数 fact は，通常 let rec を用いて， let rec fact n = if n > 0 then n * fact (n-1) else 1 と再帰的に定義されるが，次のように let rec を使わなくても定義できる．let turing (`M x) y = y (fun z -> x (`M x) y z) let fact = turing (`M turing) (fun f n -> if n > 0 then n * f (n-1) else 1) ちょっと読み難いが，実際に fact 10 と実行してみれば， 3628800 と正しい出力が得られることが確認できるだろう． このカラクリを支えている
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
