Combinadores para as funções recursivas primitivas

19

É sabido que os combinadores S e K são Turing Complete. Existem combinadores que são suficientes para produzir (apenas) as funções recursivas primitivas?

NietzscheanAI
fonte
11
É isso que você está perguntando? mathoverflow.net/questions/48006/...
Andrej Bauer

Respostas:

17

Sim, mas você deve considerar os combinadores digitados. Ou seja, você precisa fornecer a e K os seguintes esquemas de tipo: K : A B A S : ( A B C ) ( A B ) ( A C ) em que A , B e C são meta-variáveis ​​que podem ser instanciadas em qualquer tipo concreto a cada uso.SK

K:ABAS:(ABC)(AB)(AC)
A,BC

Então, você quer adicionar o tipo de números naturais para a linguagem de tipos, e adicione as seguintes combinadores: z : N s u c c : NN i t e r : N( NN ) NNN

z:Nsucc:NNiter:N(NN)NN

As regras de igualdade para as adições são:

iterifz=iiterif(succe)=f(iterife)

iter:A(AA)NA
iter

iter

pred=λk.iter(z,z)(λ(n,n).(succn,n))kpred=λk.snd(predk)

NN×N

Neel Krishnaswami
fonte
Portanto, isso é menor que Turing-completo em virtude da restrição aos combinadores digitados? As variáveis ​​de tipo (recursivamente) podem denotar funções sobre variáveis ​​de tipo (por exemplo, A = D -> E para alguns tipos D e E)?
NietzscheanAI
2
SK
Neel, obrigado. Eu estaria certo ao pensar que é possível representar z, succ e iter em termos de S e K através da codificação numérica da Igreja?
NietzscheanAI
00(succx)x
@ Xoff: a função predecessora possui uma definição de tempo linear bem conhecida em termos de iter. Este poderia ser o objeto de uma pergunta sobre cs.stackexchange.com ...
Cody