我已经编程了很长时间(实际上太长了),但我真的很难理解"自由变量"和"绑定变量"这两个术语.
我在网上找到的大多数"解释"都是从谈论Lambda演算和形式逻辑或Axiomatic Semantics等主题开始的.这让我想要伸手去拿左轮手枪.
有人可以解释这两个术语,理想情况是从实现的角度来解释.它们是否可以存在于编译语言中,以及它们转换为哪些低级代码？
使用 De Bruijn 表示法，可以将 lambda 项定义为：
data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm
或者使用通常的符号，
data Term = Var String | Lam String Term | App Term Term
这两种数据类型允许构造封闭项和包含自由变量的项。
是否可以定义仅允许构造封闭项的数据类型。即只有诸如：\xx、\x 之类的术语。xx, \x.\y. xy, \x.\y. y, \x.\y.\zz(xy)