1

これらがそれぞれの教会の数字の最も一般的なタイプである理由を理解するのに苦労しています:

2 = λf.λx. f (f x) : (α → α) → α → α 

1 = λf.λx. f x : (α → β) → α → β

0 = λf.λx. x : β → α → α

私はすべての教会の数字が同じタイプであると思っていました :

(α → α) → α → α

また、 add 演算子の一般的な型を見つけるにはどうすればよいですか

λm.λn.λf.λx. m f (n f x)

どんな助けでも本当に感謝します、ありがとう!

4

1 に答える 1

2

ゼロの教会数字から始めましょう。

λf.λx. x : β → α → α

一部だけを見るとλf.λx.、引数が 2 つの関数があると推測できます。したがって、その型はα → β → γであり、αとβは引数の型をγ表し、結果の型を表します。ここで、本体xは型をさらに制約します。関数の戻り値の型は、2 番目の引数の型と同じでなければなりません。その結果α → β → β、または名前を変更した後 (α ↔ β):になりλf.λx. x : β → α → αます。f関数であるという事実を使用しなかったため、これがゼロの最も一般的な型です。実際、型指定されていないラムダ計算のチャーチゼロ数値は気にしません。最初の引数であることを忘れているだけです。βは単なるプレースホルダーであるため、特殊化することができますα → α、これにより、ゼロのより具体的な型が得られます -- λf.λx. x : (α → α) → α → α。

見てみましょう1：

λf.λx. f x : (α → β) → α → β

繰り返しますが、これは 2 引数の関数です:α → β → γですが、今回は ( の本体を見てください) 最初の引数が関数であることが1わかっているため、 :を置き換える必要がある型があります。これで、 に適用できなければならないことがわかりました。これは、 の型との引数の型が等しくなければならないことを意味します: = 、したがって、 に到達しました。しかし、私たちが知っているのはそれだけではなく、typeを持ち、数値が returnであり、この情報を適用すると=が得られます。これらすべてを組み込むと、または名前を変更した後に到達します。ffδ → εα(δ → ε) → β → γfxxfδβ(β → ε) → β → γf xεf xεγ(β → γ) → β → γλf.λx. f x : (α → β) → α → β. ここでも、使用目的に関する情報は使用しませんでした。そのため、最も一般的な型を取得しました。もちろん、(制限β=によってα) に特殊化できますλf.λx. f x : (α → α) → α → α。

2今度は さんの番です:

λf.λx. f (f x) : (α → α) → α → α

今回はすべての手順を繰り返すわけではありませんが、(中間の手順として) に到達できますλf.λx. f (f x) : (α → β) → α → β。ただし、今回はfの結果をそれ自体にフィードしていることに注意してください: f (f x)。これは、fの入力と出力の型が等しくなければならないことを意味し、つまりβ=であり、今回αは最も一般的な型です。λf.λx. f (f x) : (α → α) → α → α

(*) Church の 、 などは、最も一般的な型と同じであることに注意してください3。4これは2、複数の関数を適用しても型をさらに特殊化するための追加情報が得られないためです。

加算関数についてはλm.λn.λf.λx. m f (n f x)、もう少し簡潔に説明します。

  • 式の型が であると仮定しますα → β → γ → δ → ε。
  • mは 2 つの引数の関数です:αに制限する必要がありますα' → α'' → α'''
  • についても同じn:βに制限する必要がありますβ' → β'' → β'''
  • mとnの最初の引数は同じ型で、次の型ですf: α'= β'=γ
  • nの 2 番目の引数の型はδ
  • nmの結果の型がの 2 番目の引数の型と等しい: β'''=α''
  • 上記のすべての知識を組み合わせてみましょうn : γ → δ → α''
  • 同じm : γ → α'' → ε
  • したがって、結果の型は(γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε

変数の名前を変更して、見栄えを良くしましょう。

の最も一般的なタイプλm.λn.λf.λx. m f (n f x)は

(β → γ → ε) → (β → α → γ) → β → α → ε.

β教会の数字 ( = α → α、γ= α、ε= α)の二項演算であると予想されるものに特化できることを確認しましょう。

((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.

于 2016-05-09T16:24:38.530 に答える