uncurry和咖喱的功能
答
假设以下definions(您需要检查那些符合你定义)
// 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
uncurry(curry E)
这导致
(λf.λp . f (first p) (second p)) ((λf.λx.λy . f (pair x y)) E)
然后就减少术语以上使用λ-caluclus的缩减规则,即使用:
- α转换:改变约束变量
- β - 还原:在应用功能,他们的论据
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
定义匹配但I th墨水,我在一些减少步骤失败。你能写下所有的步骤吗?谢谢! – ikerexxe 2013-02-14 16:23:57
我认为这是练习的要点。 – 2013-02-14 17:11:32
这样好吗? uncurry(咖喱E)= λf.λp。 f(first p)(second p)(λf.λx.λy.f(pair xy)E)= λf.λp。 f(first p)(second p)(λx.λy.E(pair xy))= λf.λp。 f(第一个p)(第二个p)E = λp。 E(首页)(第二页)= E – ikerexxe 2013-02-14 20:22:20