带 letrec、case、构造子和非确定性的 Lambda 演算
编程语言
2007-05-23 v1 人工智能
符号计算
摘要
本文研究了一种包含 case、构造子、letrec 以及（非确定性）erratic 选择的非确定性按需调用的 Lambda 演算 ，其基于重写规则。定义了作为左侧最外层归约变体的标准归约。其语义通过表达式的上下文等价性来定义，而非使用 -等价性。我们证明了若干程序转换是正确的，例如所有（确定性）的演算规则，以及垃圾回收规则、消除间接引用和唯一复制的规则。这表明，结合上下文引理与使用完整的交换（分支的）图进行的元归约，是为函数式编程语言提供语义并证明程序转换正确性的有用且成功的方法。
引用
@article{arxiv.cs/0011008,
title = {A Lambda-Calculus with letrec, case, constructors and non-determinism},
author = {Manfred Schmidt-Schauß and Michael Huber},
journal= {arXiv preprint arXiv:cs/0011008},
year = {2007}
}