「let rec」を使用せずに y-combinator を定義するにはどうすればよいですか?

Question

ほとんどすべての例で、ML タイプの言語の y コンビネータは次のように記述されます。

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

これは期待どおりに機能しますが、次を使用して y-コンビネータを定義するのは不正行為のように感じます。 let rec ....

このコンビネータを再帰を使用せずに、標準の定義を使用して定義したいと思います。

Y = λf·(λx·f (x x)) (λx·f (x x))

直訳すると以下の通りです。

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

ただし、F# は型を理解できないと不平を言います。

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a
    'a    
but given a
    'a -> 'b    
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

を使用せずに F# で y コンビネーターを記述するにはどうすればよいですか? let rec ...?

Answer 1

コンパイラのポイントアウトとして、その表現xは、よく入力されていることを(x x)に割り当てることができます何のタイプが存在しない（これは厳密には正しくありません。あなたは、明示的xとしてobj->_を入力することができます - 私の最後の段落を参照してください）。非常によく似た表現が動作するようにあなたが再帰タイプを宣言することでこの問題を回避することができます：

type 'a Rec = Rec of ('a Rec -> 'a)

次に、Yコンビネータのように書くことができる：

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

F＃が厳しい言語であるため、残念ながら、あなたは、これは非常に便利ではないことがわかります、 あなたがこのコンビネータを使って定義しようという任意の関数は、スタックオーバーフローが発生します。 代わりに、あなたはY-コンビネータ（\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))）の応用的オーダーのバージョンを使用する必要があります：

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

別のオプションは、通常のオーダーYコンビネータを定義するには、明示的な怠惰を使用することです。

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

これは再帰関数の定義は今（Valueプロパティを使用して）怠惰な値の明示的な力を必要とするという欠点を持っています

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

しかし、それはあなたがちょうどあなたが怠惰な言語では可能性として、非機能再帰的な値を定義することができるという利点があります：

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

は、最終的な別の方法として、あなたはより良いボクシングおよびダウンキャストを使用して型なしラムダ計算を近似しようとすることができます。これは（再びYコンビネータの応用的オーダーのバージョンを使用して）あなたを与えるだろう。

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

これは、それが不要なボクシングとアンボクシングの原因となることを明らかな欠点がありますが、少なくとも、これは実装に完全に内部にあり、実行時に実際に故障につながることはありません。

Answer 2

私はそれは不可能だと言い、その理由を尋ねると、手を振って、単純に型付けされたラムダ計算には次の性質があるという事実を持ち出します。 正規化プロパティ. 。つまり、単純型ラムダ計算のすべての項が終了します (したがって、単純型ラムダ計算では Y を定義できません)。

F# の型システムは、単純に型付けされたラムダ計算の型システムとまったく同じではありませんが、十分に近いものです。F#なし let rec これは、単純に型付けされたラムダ計算に非常に近いものです。繰り返しになりますが、その言語では終端しない項を定義することはできず、Y の定義も除外されます。

言い換えれば、F# では、「let rec」は少なくとも言語プリミティブである必要があります。他のプリミティブから定義できたとしても、この定義を入力することはできないからです。これをプリミティブとして持つと、とりわけ、そのプリミティブに特別なタイプを与えることができます。

編集：kvb は、型定義 (単純に型付けされたラムダ計算には存在しない機能の 1 つですが、let-rec-less F# には存在します) によって、ある種の再帰が可能になることを回答の中で示しています。非常に賢い。

Answer 3

ケースおよびMLデリバティブの文は、それはチューリング完全にするものです聞かせて、私は彼らがシステムFに基づいており、単純にタイプされていないが、ポイントが同じであると信じています。

システムFは、それができれば、それは強く正規化ではなかった、任意の不動点コンビネータのためのタイプを見つけることができません。

何強く正規化手段は、任意の表現が正確に持っているということです。の1 正規形はそれ以上を削減することができない表現がある通常のフォーム、すべての式が持つ型を持たないから、この異なり、の時最大の1つの正規形、それもまったく正常な形を持っていないことができます。

型付きラムダ計算は、いままでのように、固定小数点演算子を構築することができれば、

、それは正常な形を持たないために発現させるために非常に可能であった。

もう一つの有名な定理、停止問題は、その強正規言語はチューリング完全ではないされている意味し、それはそれは、そのプログラムのチューリング完全な言語どのサブセットの（証明とは異なる）のを決定することは不可能だろうだと言いますどのような入力に停止します。言語を強く正規化された場合、それは、つまりそれ常にの停止を停止した場合、それは決定可能です。これを決めるために私たちのアルゴリズムはプログラムです。true;

これを解決するために、ML-誘導体は、ケースとシステム-Fを拡張し、これを克服するために（REC）とします。関数は、このように、それはすべての計算機能のためだけでは無名関数に依存することはもはや不可能だ、全くラムダ結石、それ以上の効果でそれらを作る、再びその定義で自分自身を参照することはできません。したがって、これらは再び無限ループに入り、そのチューリング完全性を取り戻すことができます。

Answer 4

短い答え：あなたがすることはできません。

長い答え： 単に型付きラムダ計算は強く正規化です。これは、同等のチューリングていないことを意味します。この理由は、基本的には（あなたが見つけてきたように）Yコンビネータは、いずれかのプリミティブまたは再帰的に定義されなければならないという事実に帰着します。これは単にシステムF（または単純型付き結石）で表現することはできません。この回避する方法（それはすべての後に、証明されています）がありません。 Yコンビネータますのことができますのものの、正確にあなたが望むように作品を実装します。

私はあなたが本当の教会風Yコンビネータをしたい場合は、スキームを試してみてくださいお勧めします。他のバージョンでは動作しませんように明示的怠惰を追加したり、怠惰なSchemeインタプリタを使用しない限り、上記の応用的バージョンを使用してください。 （スキームは、技術的に完全に型指定されていないではありませんが、動的に、このための良い十分である、型付けされます。）

は、強力な正規の証明のためにこれを参照してください。 http://citeseerx.ist.psu.edu/viewdoc/summary ？DOI = 10.1.1.127.1794する

はもう少し考えた後、私はかなり確信してletrecは1が行う定義された振る舞いを正確な方法は、System Fチューリングが完全になりますことをプリミティブYコンビネータを追加することです。あなたはチューリングマシンをシミュレートするためにやらなければならないことは、その後、（バイナリで解釈）整数と（ヘッドを位置決めするために）シフトとしてテープを実装しています。