currying - カレーとカレーの機能

Question

私はラムダ計算にまったく慣れておらず、次の演習を行おうとしていますが、解決できません。

uncurry(curry E) = E

誰か助けてもらえますか？

Answer 1

次の定義を想定しています（それらが自分の定義と一致するかどうかを確認する必要があります）

// creates a pair of two values
pair    := λx.λy.λf. fxy
// selects the first element of the pair     
first   := λp. p(λx.λy. x)
// selects the second element of the pair                     
second  := λp. p(λx.λy. y)
// currys f
curry   := λf.λx.λy . f (pair x y)
// uncurrys f
uncurry := λf.λp . f (first p) (second p)

あなたが示す

uncurry(curry E) = E

上記の定義をカレーに挿入し、カレーをカレーに入れます

uncurry(curry E)

これは

(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (pair x y)) E)

次に、ラムダ計算の削減ルールを使用して、つまり次を使用して、上記の項を削減します。

• α変換：束縛変数の変更
• β削減：引数に関数を適用する

http://en.wikipedia.org/wiki/Lambda_calculus http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf

これはにつながるはずです

E

各削減ステップを書き留めると、次のことが証明されます。

uncurry(curry E) = E

ここにそれがどのように見えるべきかをスケッチします：

uncurry(curry E) = // by curry-, uncurry-definion
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (pair x y)) E) = // by pair-definiton
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (λx.λy.λf. fxy x y)) E) = // 2 alpha-conversions
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (λa.λb.λf. fab x y)) E) = // 2 beta-reductions
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (λf. fxy)) E) = // ...

...
...
... = // β-reduction
E