lambda演算解释器 什么： 用C ++编写的小型lambda演算解释器。 它支持α转换和β减少，以及精确跟踪替换和重命名的输出。 如何： 支持标准的lambda演算语法，例如： (λz.(((λx.(λy.x)) z) ((λx.(λy.x)) z))) 请注意，变量名称可以是多字符，因此必须用空格分隔。 支持用于多参数函数的语法糖： λx y.x == λx.λy.x 还支持Haskell风格的lambda语法，因为没有人知道如何键入λ： \x y -> x == \x -> \y -> x 还支持let绑定： let S = \x y z -> x z (y z) let K = \x y -> x let I = \x -> x S K K == I 如果使用了FLAG_VAR_REPLACEMENT标志（与:v切换），则解释器将尝试通过使用alpha等效性FLAG_

Lambda演算评估器 介绍 这是一个简单的lambda演算评估程序，它支持以下具体语法：表达式：=标识符| （lambda标识符表达式）| 表达式表达式 为了使它真正纯净，当前不支持常量。 它应用alpha转换和beta减少来减少表达式。 此评估程序是使用C实现的。Lex和Yacc用于生成扫描器和解析器。 先决条件 除了基本的构建工具GCC和Make之外，还需要Lex和Yacc的实现来编译和运行此评估程序。 Flex和Bison在我的平台上使用。 您可以在Makefile中将其更改为您自己的。 生成并运行 将Makefile中与构建相关的变量更改为您的特定环境。 使用Make构建程序：$ make 使用以下命令运行评估程序：$ ./main 使用Ctrl + C退出评估程序。 接触 查敏杰

This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, type inference, denotational semantics, complete partial orders, and the language PCF.

个人收集的一些关于lambda演算的国内外资料和课件，请笑纳