Что такое алгоритм для перечисления лямбда-терминов?

Question

Что такое алгоритм, который будет перечислять выражения для лямбда-исчисления по порядку длины? Например, (λx.x), (λx.(x x)), (λx.(λy.x)) и так далее?

Answer 1

В длину я бы выбрал число T -разложений («глубина») в этом BNF из (нетипизированных) лямбда-выражений:

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

В питона вы можете определить генератор, следуя вышеприведенным правилам поколения для данные переменные и заданная глубина, как это:

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) 

Теперь вы можете перечислить термины лямбды для/до заданной глубины:

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 

и так далее (т.е. this sequence).