如何在ANF中對身份函數進行編碼？

Question

我正在嘗試討論ANF（管理範式），但我無法理解lambda術語的翻譯。考慮這個lambda項：λx.x。你如何在ANF中編碼？ x是一個變量，而是一個lambda體必須是一個讓約束力或ANF的功能應用，根據ANF語法：

EXP ::= VAL VAL 
     | let VAR = EXP in EXP 

VAL ::= λ VAR . EXP 
     | VAR 

Answer 1

上A-normal form的維基百科頁面無法提供完整的語法。 這裏是校正版本：

EXP ::= VAL 
     | VAL VAL 
     | let VAR = EXP in EXP 

VAL ::= λ VAR . EXP 
     | VAR 

這意味着恆等函數是A歸一化函數的一個固定點，即，它僅僅是相同λx. x。更多關於這可以找到here。