Quais funções as expressões de cálculo combinador podem calcular?

Uma expressão combinadora (digamos na base SK) pode ser pensada como uma função que mapeia expressões de cálculo combinador para expressões de cálculo combinador. Ou seja, pode-se pensar em uma expressão $X$ como uma função $X:L \to L$ , onde $L$ é o conjunto de todas as expressões combinadoras sintaticamente válidas na base SK. Esse mapeamento é realizado aplicando a entrada à expressão e depois reduzindo para a forma normal para obter a saída.

Como a base SK é Turing completa, pode-se ingenuamente pensar que existe uma uma SK expressão que implementa qualquer função computável de a . No entanto, isso claramente não é o caso, pois o resultado da redução sempre estará na forma normal. Isso significa que não há como uma expressão ter uma saída que não esteja na forma normal. $X$ $L$ $L$

Então, em vez disso, eu poderia pensar nas expressões de cálculo SK como mapeando para , onde é o conjunto de expressões SK na forma normal. É o caso de que, para qualquer mapa computável , existe uma expressão SK que implementa esse mapa? Ou existem outras restrições no conjunto de funções que podem ser calculadas por expressões de cálculo combinador dessa maneira? $L'$ $L'$ $L'$ $f:L'\to L'$ $X$

lambda-calculus combinatory-logic Nathaniel
fonte

Respostas:

Para fazer a bola rolar, e na esperança de outras pessoas dar respostas mais profundas e detalhadas sobre a estrutura das funções definíveis , deixe-me citar o Corolário 20.3.3 do The Lambda Calculus de Barendregts , sua sintaxe e Semântica (também conhecida como "a Bíblia"). $\lambda$ $L'\to L'$

Corolário 20.3.3: A função , definido por não é definível no untyped - cálculo, ou seja, não existe um termo tal que $\delta:L'^2\to L'$
$δ (M, N) = {\begin{cases} T r você e E se M =_{β η} N \\ F uma eu s e de outra forma \end{cases}$ $\delta(M, N) = \cases{\mathrm{True}\mbox{ if }M=_{\beta\eta}N\\ \mathrm{False}\mbox{ otherwise}}$ $\lambda$ $D$ $D M N =_{β η} δ (M, N)$ $D\ M\ N =_{\beta\eta} \delta(M,N)$ para todos os . $M,N\in L'$

A prova envolve considerações nas árvores de Böhm, que fornecem uma caracterização bastante forte das possíveis "ações" de termos arbitrários de lambda em formas normais. Em particular, para qualquer termo fechado não constante , on pode encontrar e modo que $F$ $n\in\mathbb{N}$ $P_1,\ldots,P_n$

F x P_{1} ... P_{n} =_{β η} x Q_{1} ... Q_{k}

$F\ x\ P_1\ldots P_n =_{\beta\eta} x\ Q_1\ldots Q_k$

$k$ $Q_1,\ldots,Q_k$ $D$ $\delta$ $D$

cody
fonte