如何在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。