Lambda微積分免費可變問題

我發現邁克戈登的功能性編程介紹Notes在網絡上，我試圖通過它。第9頁有這樣的疑問：Lambda微積分免費可變問題

Find an example to show that if V1 = V2 , then even if V2 is not free in E1, 
it is not necessarily the case that: 

(λ V1 V2 . E) E1 E2 = E [E1/V1][E2/V2]

我猜，我可以說，因爲V1和V2是平等的，我們可以這樣重做：

(λ V2 V1 . E) E1 E2

，因此說

(λ V1 . E[E1/V2]) E2

給出了V2在E1中不空閒的規定。但是，我們不能說

E[E1/V2][E2/V1]

因爲E2必然有V1免費。或者我錯過了什麼？

來源

2013-03-24 user2054900

這不是一個反例。除此之外，我不明白你最後一步的推理 - 爲什麼V1必須在E2中自由發生？除此之外，在你最後一步E[E1/V2][E2/V1]不是一個聲明。你是什麼意思？「我們不能說那E[E1/V2][E2/V1]？」

你應該嘗試構建明確反了這一假說，即選擇V1=V2=x（它其實並不重要，因爲α轉換），然後找到明確表達E，E1，E2使得它們滿足假設的假設（V2不在E1中免費），但表達式`E[E1/V2][E2/V2]不等於(λV1 V2. E) E1 E2的減少。

既然你說過你想自己做這個，我不會給你解決方案，但可以隨時索要更多的指針。

來源

2013-03-24 23:00:08

似乎在說'（v1 v1 v2。E）E1 E2 = E [E1/V1] [E2/V2]'其中'v1'和'v2'是不同的，就像是說例如'λv1。（λv2。v1）E1 E2'，它可以測試到'（λv2。E1）E2'，這將只是'E1'。但是如果我們試圖用'v1 = v2'來表示原始的redex或者只是'v'，使用我們的例子：'λv。（λv。v）E1 E2'這將是beta到E2，這是一個矛盾。因此，（一般情況下）你不能使用alpha'λv1 v2。 E'到'λv v。 E'。 – user2054900 2013-03-25 04:09:41

Lambda微積分免費可變問題

回答

相關問題