Term "pożerający dowolną ilość argumentów"

C = λfx.ff
R = λx.CC

Ra → CC = (λfx.ff)C → λx.CC = R

Zadanie domowe 1:

R = λfx.x(λx.ffx)
M = λx.RRx
MN → RRN → N(λx.RRx) = NM

Notes:

(v1) Izomorfizm Curry'ego-Howarda: Rachunek λ z typami prostymi i minimalna logika implikacyjna to to samo.

prawo Pierce'a: ( (p → q) → p ) → p

Tw Pottingera: termy SN <=> typowalne w typach iloczynowych.

System F:

G |- A X. P(X)

--------------

 G |- P(\phi)

\phi - formuła z wyróżnioną  zmienną wolną.

W systemie F typowalne są wszystkie funkcję, których dowód totalności jest w arytmetyce drugiego rzędu.

Tw. (Joe Wells, 1993)

Problem typowalności i problem sprawdzania typu w systemie F są nierozstrzygalne.

Tw (Gabbay/Sobolew, Loob)

Nierozstrzygalne jest pytanie: "dane t, czy istnieje term zamknięty M typu t"

(równoważnie: czy t jest twierdzeniem intuicjonistycznej logiki zdaniowej)

Tw (o poprawności redukcji w systemie F w wersji Curry'ego)

Jeśli G |- M : t oraz M ->> N, to G |- N : t

(Uwaga! Nie działa dla eta redukcji)

Dobra Nowina (Jean-Yves Girard, 1971)

System F ma własność SN. (dowód musi być w arytmetyce III-rzędu).