枚举 lambda 项的算法是什么？答案

【问题标题】：What is an algorithm to enumerate lambda terms?枚举 lambda 项的算法是什么？
【发布时间】：2014-01-09 05:54:43
【问题描述】：

什么是按长度顺序枚举 lambda 演算表达式的算法？比如(λx.x), (λx.(x x)), (λx.(λy.x))等等？

【问题讨论】：

如何定义长度？
@KristopherMicinski 任何命令都可以，我不是故意要严格这个词。我只是想避免明显的灾难，例如在(λx.λy.y)之前生成(λx.(λy.(λz.((z x) (y x) x y y))))，这显然是错误的。

标签： algorithm functional-programming lambda-calculus

【解决方案1】：

作为长度，我会在这个（无类型的）lambda 表达式的 BNF 中选择T-expansions（“深度”）的数量：

V ::= x | y
T ::= V    | 
      λV.T |
      (T T)

在 python 中，您可以按照上述生成规则为给定变量和给定深度定义生成器，如下所示：

def lBNF(vars, depth):
  if depth == 1:
    for var in vars:
      yield var
  elif depth > 1:
    for var in vars:
      for lTerm in lBNF(vars,depth-1):
        yield 'l%s.%s' % (var,lTerm)
    for i in range(1,depth):
      for lTerm1 in lBNF(vars,i):
        for lTerm2 in lBNF(vars,depth-i):
          yield '(%s %s)' % (lTerm1,lTerm2)

现在您可以枚举/达到给定深度的 lambda 项：

vars = ['x','y']
for i in range(1,5):
  for lTerm in lBNF(vars,i):
    print lTerm

【讨论】：

很好的答案，谢谢！是否可以使用 bruijn 索引对其进行修改，使其仅生成封闭项？
@viclib 你的意思是没有未绑定的变量？（从未听说过 bruijn 指数）这需要一些后处理 - 或其他一些智能适应......
嗯嗯，这只是一种扔字符串的方式。 (λ(λ(0 1))) - 这里，0 绑定到第二个 λ，1 绑定到拳头。

【解决方案2】：

参见https://arxiv.org/abs/1210.2610，第 5 页。以下是一些示例代码：

from itertools import chain, count
from functools import lru_cache

@lru_cache(maxsize=None)
def terms(size, level=0):
    if size == 0:
        return tuple(range(level))
    else:
        abstractions = (
            ('abs', term)
            for term in terms(size - 1, level + 1)
        )
        applications = (
            ('app', term1, term2)
            for i in range(size)
            for term1 in terms(i, level)
            for term2 in terms(size - 1 - i, level)
        )
        return tuple(chain(abstractions, applications))

def string(term):
    if isinstance(term, tuple):
        if term[0] == 'abs':
            return '(λ {})'.format(string(term[1]))
        elif term[0] == 'app':
            return '({} {})'.format(string(term[1]), string(term[2]))
    else:
        return term

for size in count():
    print('{} terms of size {}'.format(len(terms(size)), size))
    for term in terms(size):
        pass # input(string(term))

这个输出

0 terms of size 0
1 terms of size 1
3 terms of size 2
14 terms of size 3
82 terms of size 4
579 terms of size 5
4741 terms of size 6
43977 terms of size 7
454283 terms of size 8

等等（即this sequence）。

【讨论】：