作者etwas (i'm only dust)
看板PLT
标题[问题] abstration in combinatory logic
时间Wed Jun 8 03:30:54 2011
大家好,
小弟在看 Hindley & Seldin 的 Lambada-Calculus and Combinators -- an Introduction
遇到一个问题
想请教各位大大.
Exercise 2.22 里面要 evaluate
[x].uxxv
答案是
S(SuI)(Kv)
根据的是
Definition 2.18(Abstraction) for combinatory logic terms
(a) [x].M ≡ KM if x FV(M);
(b) [x].x ≡ I;
(c) [x].Ux ≡ U; if x FV(U);
(d) [x].UV ≡ S([x].U)([x].V) if either (a) nor (c) applies.
假如apply不同的rule会得到不同的答案
e.g.
[x].uxxv
≡ S([x].ux)([x].xv) by (d)
≡ Su([x].xv) by (c)
≡ Su(S([x].x)([x].v)) by (d)
≡ Su(SI(Kv))
除了definition 明写 (d)需要是if either (a) nor (c) applies
我没有读到有其他的限制
所以不知道是不是本来就是apply不同的rule会得到不同的答案
谢谢
--
'TIS better to be vile than vile esteem'd
~William Shakespeare
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 188.74.78.60
1F：→ etwas:(a)和(c) 的是 if x doesn't occur in FV(M) 和 06/08 03:36
2F：→ etwas:if x doesn't occur in FV(U) 06/08 03:37
3F：→ etwas:呃 doesn't belong to FV... 06/08 03:44
4F：推 SansWord:这是parse问题， [x].uxxv 实际ast是？ 06/24 12:43