我的 Lambda 微积分语法是否明确？答案

【问题标题】：Is My Lambda Calculus Grammar Unambiguous?我的 Lambda 微积分语法是否明确？
【发布时间】：2013-02-16 16:47:03
【问题描述】：

我正在尝试为处理 lambda 演算的语言编写一个小型编译器。这是我发现的语言的模棱两可的定义：

E → ^ v . E  | E E | ( E ) | v

符号 ^, ., (, ) 和 v 是记号。 ^ 表示 lambda，v 表示变量。 ^v.E 形式的表达式是函数定义，其中 v 是函数的形参，E 是函数体。如果 f 和 g 是 lambda 表达式，则 lambda 表达式 fg 表示函数 f 对参数 g 的应用。

我正在尝试为这种语言编写一个明确的语法，假设函数应用程序是左关联的，例如 fgh = (fg)h，并且函数应用程序的绑定比 . 更紧密，例如 (^x. ^y.xy) ^zz = (^x.(^y.xy)) ^zz

这是我目前所拥有的，但我不确定它是否正确：

E -> ^v.E | T
T -> vF | (E) E
F -> v | epsilon

有人可以帮忙吗？

【问题讨论】：

1) 明确的语法不是万能的。
2) 为什么要手动而不是使用（免费）语法工具，其中许多工具可以在网络上免费获得？
介意给我指一个好的吗？我对此很陌生。
irony.codeplex.com 易于学习。
@Pieter 出于许多实际目的，语法必须是明确的。更多的解析树会产生不止一种解释，这在翻译口语时可能没问题，但这不是常态。

标签： parsing lambda programming-languages grammar lambda-calculus

【解决方案1】：

在阅读您的问题和 cmets 之间，您似乎更多地寻求学习和实施 lambda 演算的帮助，而不仅仅是您在此处提出的具体问题。如果是这样，那么我在同一条路上，所以我会分享一些有用的信息。

本杰明·C·皮尔斯 (Benjamin C. Pierce) 的《Types and Programming Languages》(WorldCat) 是我所拥有的最好的书，这并不是说最好的书。我知道标题听起来不像 lambda 演算，但请看一下λ-Calculus extensions: meaning of extension symbols，它列出了本书中的许多 lambda 演算。这本书的代码在OCaml和F#。

尝试在CiteSeerX 中搜索有关 lambda 演算的研究论文以了解更多信息。

目前我发现的最好的 λ-Calculus 评估器是：

Lambda calculus reduction workbench 与信息here。

另外，我发现您可以在 CS:StackExchange 获得与编程相关的 lambda 演算问题以及在 Math:StackExcahnge 获得的数学相关问题更好的答案。

关于实现 lambda 演算的编程语言，如果您还没有，您可能需要学习 functional language；是的，它是另一种野兽，但在山的另一边的启蒙是壮观的。我发现的大多数源代码都使用了一种函数式语言，例如 ML 或 OCaml，一旦你学会了一种，其余的就会变得更容易学习。

更具体地说，here 是无类型 lambda 演算项目的源代码，here 是 YACC 的 F# 变体的输入文件，从阅读您之前的 questions 来看，它似乎在您的世界中知识，here 是样本输入。

由于该语法用于实现 REPL，因此它从顶层开始，认为命令提示符，并接受多个命令，在这种情况下是 lambda 演算表达式。由于该语法用于许多演算，它在前面的示例中具有占位符的部分，因此这里的绑定更多是占位符。

终于到了你想要的部分

注意 LCID 是小写标识符

Term : AppTerm
     | LAMBDA LCID DOT Term 
     | LAMBDA USCORE DOT Term 

AppTerm : ATerm   
        | AppTerm ATerm

/* Atomic terms are ones that never require extra parentheses */
ATerm : LPAREN Term RPAREN 
      | LCID

【讨论】：

感谢您的回答。我对您提供的语法中的 USCORE 术语有点困惑 - 这似乎不是我上面指定的语言的一部分。此外，您提供的语法似乎是左递归的，这是我目前试图避免的。你能评论一下我写的语法的有效性吗？
@JohnRoberts 在回答之前我将不得不更多地研究 USCORE，我使用了该项目中的一些其他语法。正如 Pieter Geerkens 所说，不要沉迷于语法。很久以前我做过同样的事情，现在我专注于 AST 并使用许多解析器之一，即 LL、LR、解析器组合、手动构建递归下降等来创建 AST。为了确定您的语法是否模糊，您需要指定它们的解析器类型。这个语法是为 LR paser 准备的，但你似乎在学习 LL 语法，不是吗？
我正在寻找 LALR(1) 解析器语法 - 我只是先检查 LL(1) 作为快速验证。再看我的语法，在我看来，它无法处理字符串末尾带括号的表达式的情况，例如 λx.λy.λz.x (yz) - 你也看到了吗？
注意：约翰和我使用了一个聊天室来继续这个过程。 chat.stackoverflow.com/rooms/25426/lambda-calculus

【解决方案2】：

您可能会在亚线性时间内找到特定语法歧义的证明，但证明语法明确是一个 NP 完全问题。您必须生成该语言中所有可能的句子，并检查每个句子是否只有一个派生词。

【讨论】：