什么是枚举 lambda 项的算法

Question

什么是

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

Answer 1

作为长度，我会选择这个（非类型）lambda 表达式的 BNF 中的T扩展（"深度"）的数量：

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

Answer 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

等等（即这个序列）。