Reprezentacja liczb naturalnych w rachunku lambda.pdf

(95 KB) Pobierz
Reprezentacja liczb naturalnych w rachunku lambda
-Term λsx.x reprezentuje liczbę naturalną 0.
-Term λsx.s(s(...(sx)...)) gdzie s występuje n razy
reprezentuje liczbę naturalną n.
Mówimy, że term E rachunku lambda reprezentuje
funkcję na liczbach naturalnych
e
:
N
k
N
wtw gdy
E n
1
....
n
k
�½

e
n
1
,...,
n
k
, gdzie
n
oznacza reprezentację
liczby n w rachunku lambda.
Operacje na liczbach
Term A=λmnsx.(ms)(nsx) reprezentuje dodawanie
liczb naturalnych.
Term M=λmnsx.n(ms)x reprezentuje mnożenie liczb
naturalnych.
Term C=λmnksx.m(λy.nsx)(ksx) reprezentuje funkcję
if...then.z..else, która oczekuje na podanie trzech
argumentów m,n i k. W przypadku gdy m jest zerem
zwraca liczbę k, w przeciwnym wypadku zwraca
liczbę n.
e
m, n
�½
n
m
.
Term E=λmn.(mn) reprezentuje funkcję
Term
P
�½
n
.
n
z
.
A
1
z
0
,
z
0
0, 0
1
, gdzie A oznacza
term dodawania, z jest parą uporządkowaną, której
pierwsza składowa to
z
0
, natomiast druga to
z
1
reprezentuje poprzednik.
Beztypowy rachunek lambda to model obliczeń
równoważny funkcjom rekurencyjnym (obliczalnym).
Aby móc dowolną funkcję rekurencyjną
reprezentować w rachunku lambda konieczne jest
wprowadzenie operatora punktu stałego y. Operator
punktu stałego to term, który dla dowolnego termu M
daje jego punkt stały tzn.
YM
�½
M
YM
.
Term Y=λy.(λx.y(xx))(λx.y(xx)) jest oczekiwanym
operatorem.
Typowany rachunek lambda
Zakładamy, że mamy nieskończony, przeliczalny
zbiór zmiennych (różnych od zmiennych ze zbioru
Var). Typ to wyrażenie zdefiniowane indukcyjnie:
-każda zmienna jest typem, zwanym typem
atomowym.
-jeżeli σ i τ są typami, to
jest typem, zwanym
typem złożonym.
Termom nadajemy typy w następujący sposób:
-jeżeli term M jest pojedynczą zmienną typu τ, to M
jest typu τ.
-jeżeli term M=λx:τ.N:σ, to M jest typu
.
-jeżeli term M=PQ, gdzie P jest typu
, a Q-typu
τ, to M jest typu σ.

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin