Zadanie 1
Napisz termy reprezentujące następujące funkcje:
Wskazówka: Funkcje
,
i
są reprezentowane odpowiednio przez termy
, i :
Zadanie 2
Napisz termy definiujące funkcję kodującą parę liczb oraz
funkcje rozkodowujące.
Wskazówka: Poniższe termy reprezentują funkcję kodującą (term
) oraz funkcje rozkodowujące (termy
i
):
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned I & = & \lambda mn stx. (ms)(ntx)\\ R & = & \lambda z sx. z(\lambda y.y)sx\\ L & = & \lambda z sx. zs(\lambda y.y)x. \endaligned}
Kodem pary
liczb jest funkcja, która czeka na podanie dwóch argumentów:
jeżeli pierwszy z nich jest identycznością, to funkcja zwraca , jeżeli
drugi, to .
Sprawdźmy jak działają termy , i na przykładzie. Kodem pary
jest:
Prawą współrzędną liczymy, używając termu :
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned R (I \underline{2}\ \underline{1}) & =_\beta & \lambda sx. (I \underline{2}\ \underline{1})(\lambda y.y) sx\\ & =_\beta & \lambda sx. (\lambda y.y) ((\lambda y.y)(sx))\\ & =_\beta & \lambda sx. sx\\ & = & \underline{1} \endaligned}
a lewą - termu :
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned L (I \underline{2}\ \underline{1}) & =_\beta & \lambda sx. (I \underline{2}\ \underline{1})s (\lambda y.y) x\\ & =_\beta & \lambda sx. s(s((\lambda y.y)x))\\ & =_\beta & \lambda sx. s(sx)\\ & = & \underline{2} \endaligned}
Zadanie 3
Niech funkcje oraz będą lambda definiowalne
odpowiednio przez termy , , ..., , a jednoargumentowa funkcja
przez term . Napisz termy reprezentujące funkcje:
Wskazówka:
Niech będzie funkcją następnika. Wówczas .
Sprawdźmy, jak działa term :
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned F_2 \underline{1}\ \underline{2} & = & \underline{2}\ T \underline{1}\\ & =_\beta & (\lambda sx. s(sx))T \underline{1}\\ & =_\beta & T( T\underline{1})\\ & ... & \\ & =_\beta & \lambda sx. s(s(sx))\\ & = & \underline{3} \endaligned}
Zadanie 4
Napisz term reprezentujący funkcję .
Wskazówka: Funkcja
daje się zapisać jako:
Punkt stały termu
czyli , reprezentuje funkcję .
Sprawdźmy na kilku przykładach, czy tak jest rzeczywiście:
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned ({\cal Y} F)\underline{0} & = & F({\cal Y} F)\underline{0}\\ & =_\beta & \underline{1}\\ \\ ({\cal Y} F)\underline{1} & = & F({\cal Y} F)\underline{1}\\ & =_\beta & (({\cal Y} F)\underline{0})\cdot \underline{1}\\ & =_\beta & \underline{1}\\ \\ ({\cal Y} F)\underline{2} & = & F({\cal Y} F)\underline{2}\\ & =_\beta & (({\cal Y} F)\underline{1})\cdot \underline{2}\\ & =_\beta & \underline{1}\cdot \underline{2}\\ ... \endaligned}
Zadanie 5
Napisz term reprezentujący funkcję Fibonacciego:
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned f(0) & = 1\\ f(1) & = 1\\ f(n+1) & = f(n) + f(n-1) \endaligned }
Wskazówka: Punkt stały termu
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned F & = \lambda f n. \quad if \quad n=0\ then\ 1\ else\\ & if\ n-1 = 0\ then\ 1\\ & else\ f(n - 1) + f(n-2), \endaligned }
czyli , reprezentuje funkcję .
Sprawdźmy na przykładzie, czy tak jest rzeczywiście:
Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned ({\cal Y} F)\underline{2} & = \quad F({\cal Y} F)\underline{2}\\ & =_\beta \quad (({\cal Y} F)\underline{1}) + (({\cal Y} F)\underline{0})\\ & =_\beta \quad \underline{1} + \underline{1} \endaligned}
Zadanie 6
Jakiego typu są poniższe termy:
Zadanie 7
Podaj przykładowe termy (jeśli takowe istnieją) dla poniższych typów.