Что такое отображение между натуральными числами и действительными просто типизированными терминами лямбда-исчисления?

Question

Есть ли эффективный алгоритм, который отображает между хорошо типизированными замкнутыми членами просто типизированного лямбда-исчисления и натуральными числами? Например, с помощью Брейна индексов (и, вероятно, на неправильном порядке):

0 → (λ 0) 
1 → (λ (λ (0 1))) 
2 → (λ (λ (1 0))) 
3 → (λ 0 (λ 0)) 
4 → (λ (λ 0) 0) 
5 → (λ (λ 1) 0) 
6 → ... so on 

Похожие вопросы: существует ли алгоритм, который отображает между натуральными числами и нормированных с точки зрения простого типизированного лямбда-исчисления? Кроме того, те же вопросы относятся к нетипизированному лямбда-исчислению.

Answer 1

Бинарное исчисление лямбда определяет двоичное кодирование для любого закрытого члена в нетипизированном лямбда-исчислении, а также предлагает биекцию между натуральными числами и двоичными строками, но первая не является сюръективной. Тем не менее, статья http://arxiv.org/abs/1401.0379 «Условия подсчета в бинарном исчислении лямбда» может давать эффективные сопоставления ранжирования/без учета.

Answer 2

Из-за очень контекстно-зависимой природы типизированного лямбда-исчисления я был бы удивлен, если бы был эффективный алгоритм, или, скорее, «естественный» эффективный алгоритм.

This paper имеет хорошие формулы для подсчета нетипизированных терминов лямбды и от этого они получают довольно простую функцию для перечисления нетипизированных терминов. Они также обеспечивают функцию счета для нормальных форм, которые также легко адаптировать к генерирующей функции. К сожалению, они делают только функцию типизированного генератора, фильтруя то, что абсурдно дорого (один из результатов статьи - насколько это абсурдно).

Что касается более эффективного способа генерации типизированных терминов, то я бы посоветовал генерировать , вводя типы вместо терминов, а затем набирать их.