haskell - 如何对二进制 lambda 演算的输出建模？

Question

我正在尝试为 John Tromp's binary lambda calculus 编写一个解释器

我已经编写了代码来执行以下操作:

1. 将二进制输入解析为表示常规无类型 lambda 演算的某种数据结构
2. Beta-减少这个词

然后会发生什么？

• 如何解释“输出”？
• 是输出
  • a) 通过相同的编码将生成的术语翻译回二进制，
  • 或 b) 由假终止 bool 值列表编码的比特流？
• (如果输出没有形成这样的列表会怎样？)

还是我误解了 BLC 的工作原理？

Answer 1

我建议使用 http://www.ioccc.org/2012/tromp/hint.html作为您的主要引用。维基百科页面可能还不错，但他在 BLC 上的原始笔记相当不错。

关于输入输出的话题，他是这样说的:

More specifically, it defines a universal machine, which, from an input stream of bits, parses the binary encoding of a lambda calculus term, applies that to the remainder of input (translated to a lazy list of booleans, which have a standard representation in lambda calculus), and translates the evaluated result back into a stream of bits to be output.