Kombinatory dla pierwotnych funkcji rekurencyjnych


Odpowiedzi:


17

Tak, ale musisz wziąć pod uwagę kombinatory maszynowe. Oznacza to, że musisz podać i następujące schematy typów: gdzie i są meta-zmiennymi, które mogą być tworzone przy użyciu dowolnego konkretnego typu przy każdym użyciu.K K : A B A S : ( A B C ) ( A B ) ( A C ) A , B CSK

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

Następnie chcesz dodać typ liczb naturalnych do języka typów i dodać następujące kombinatory: z : N s u c c : NN i t e r : N( NN ) NNN

z:Nsucc:NNiter:N(NN)NN

Reguły równości dla dodatków to:

iterifz=iiterif(succe)=f(iterife)

O wiele łatwiej jest czytać pisane programy, jeśli po prostu piszesz programy w prostym typie rachunku lambda, powiększonego o cyfry i iterację. System, który opisałem, jest ograniczeniem T Goedela , języka arytmetyki wyższego typu. W Goedel's T wpisywanie iteracji jest mniej ograniczone: W T , możesz utworzyć na dowolnym typie, a nie tylko na liczbach naturalnych. To prowadzi Cię do prymitywnej rekurencji i pozwala zdefiniować takie rzeczy, jak funkcja Ackermana.

iter:A(AA)NA
iter

EDYCJA: Xoff zapytał, jak zakodować funkcję poprzednika. Wynika to standardową lewą. Aby to wyjaśnić, użyję do tego notacji lambda (którą można wyeliminować za pomocą abstrakcji nawiasów), ponieważ jest to o wiele bardziej czytelne. Najpierw załóżmy, że mamy pary i bardziej ogólny typ dla . Następnie możemy zdefiniować:iter

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

Jeśli masz tylko iterator typu nat, musisz wykorzystać izomorfizm, który , co jest denerwujące, ale nie stanowi podstawowej przeszkody.NN×N


Czyli jest to mniej niż ukończenie Turinga ze względu na ograniczenie do kombinatorów maszynopisanych? Czy zmienne typu (rekurencyjnie) mogą oznaczać funkcje nad zmiennymi typu (np. A = D -> E dla niektórych typów D i E)?
NietzscheanAI

2
SK

Neel, dzięki. Czy miałbym rację, myśląc, że możliwe jest reprezentowanie z, succ i iter w kategoriach S i K za pomocą kodowania liczbowego Kościoła?
NietzscheanAI

00(succx)x

@Xoff: funkcja poprzednika ma dobrze znaną definicję czasu liniowego pod względem iter. To może być przedmiotem pytania na cs.stackexchange.com ...
cody
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.