如何使用命名上下文來查找de Bruijn指數的自由變量？

在「類型和編程語言」中，第6.1.2節中他們討論了用於爲lambda表達式中的自由變量編號的命名上下文。使用他們提供的示例方案，λx.xb和λx.xx的de Bruijn表示形式爲λ.00，如果它們有明顯不同的術語。這個怎麼用？如何使用命名上下文來查找de Bruijn指數的自由變量？

來源

2012-02-26 sanjoyd

什麼讓你覺得第一個的表示將是'λ.00'。我不認爲第一個可以表示出來，因爲'b'沒有被綁定到任何地方。 – sepp2k 2012-02-26 04:06:49

在我提到的部分中，他們討論瞭如何使用_naming context_表示自由變量。 – sanjoyd 2012-02-26 04:27:05

啊，我明白了。我會盡快寫一個答案。 – sepp2k 2012-02-26 04:42:41

至於你提到書中使用從0到數字n自由變量映射到n-1命名上下文。但是，如果仔細觀察本書中的示例，您會注意到它並不直接使用這些數字來表示變量。例如，它代表了λw. y w爲λ. 4 0即使對於y映射是3，不是4

這裏發生的事情是，他增加了變量數目的嵌套深度。即如果自由變量v嵌套在d lambdas中，它將獲得索引Γ(v)+d，而不僅僅是Γ(v)。

因此在您的示例中，使用上下文Γ {b -> 0}λx.xb將表示爲λ. 0 1而不是λ. 0 0。因此沒有歧義。

來源

2012-02-26 05:04:12 sepp2k

爲了學習Lambda微積分的工作原理，我創建了一個基於網絡的解釋器（http://pure-fn.appspot.com/about），以獲得更簡單的基於索引的方法。我會很感激你對此的反饋。 – dansalmo 2013-03-22 18:58:34

如何使用命名上下文來查找de Bruijn指數的自由變量？

回答

相關問題