Johdatus lambdakalkyyliin

lista sisältää 0–n elementtiä, jotka voivat olla mitä tahansa tietoja
rakennetaan induktiivisena tietotyyppinä
- lista on joko tyhjä (0 elementtiä), tai sitten solu, johon on talletettu listan ensimmäinen elementti ja loput listasta
- muodollisesti: list ::= nil | cell element list
- element on mitä tahansa tyyppiä (ohjelmoijan vastuulla)
toteutus kuten muillekin induktiivisille tietotyypeille:
- nil =(def) λ n c. n
- cell =(def) λ e r. λ n c. c e r

kun meillä on lista l, se voi siis olla tyhjä lista tai solu
listaa esitetään tarkasteluoperaatiolla eli listalle annetaan kaksi argumenttia, joista se kutsuu jompaakumpaa sen mukaan, onko se tyhjä
- solun tapauksessa elementti ja listan loppuosa annetaan argumenteiksi
esimerkiksi (λ l. l 0 (λ e r. e))
- (λ l. l 0 (λ e r. e)) nil → (λ n c. n) 0 (λ e r. e) → 0
- (λ l. l 0 (λ e r. e)) (cell 1 nil) →
  (λ n c. c 1 nil) 0 (λ e r. e) →
  (λ e r. e) 1 nil → 1

Muista: list ::= nil | cell element list
- nil =(def) λ n c. n
- cell =(def) λ e r. λ n c. c e r
elementtien poiminta
- head = λ l. l Ω (λ e r. e)
- tail = λ l. l Ω (λ e r. r)
- first = λ l. head l = head
- second = λ l. head (tail l)
- third = λ l. head (tail (tail l))
yleinen periaate: otetaan listasta (n-1) kertaa häntä ja sitten siitä ensimmäinen elementti
- tämä yleistetään rekursiolla myöhemmin

tuottaa uuden listan uudella sisällöllä
elementin vaihtaminen
- replace-first = λ e l. cell e (tail l)
- replace-second = λ e l. cell (first l) (cell e (tail (tail l)))
- replace-third = λ e l. cell (first l) (cell (second l) (cell e (tail (tail (tail l)))))
Yleinen periaate: rakennetaan lista, jossa on ensin n elementtiä vanhasta, sitten uusi elementti, sitten vanhan häntä
- Listat jakavat hännän!
- Ei ongelma: tietorakenteisiin ei tehdä koskaan muutoksia, joten yhtä tietorakennetta voi käyttää monen muun osana

rekursio on induktiivisen tietotyypin luonnollinen käsittelytapa
tietotyyppiä käsittelevässä funktiossa on oma käsittelytapansa jokaiselle muodostimelle
- koska tietotyyppi mallinnetaan tarkasteluoperaationa, kutsutaan siis tietotyyppiä ja annetaan sille argumenteiksi, mitä palautetaan minkin muodostimen ollessa kyseessä
niissä muodostimissa, joissa viitataan samaan tietotyyppiin induktiivisesti, funktio käyttää laskentaan itseään rekursiivisesti
- myös luvuilla on luontainen rakenteellinen rekursio

jokaisen rekursiivisen määritelmän voi kirjoittaa Y-kombinaattorilla ei-rekursiivisesti
- tarvitsemme määritelmän muotoa: xxx = … xxx …
- λ-kalkyylissa sanomme: xxx = Y (λ i. … i …)
- esim. forever-false = Y (λ i. cell false i)
jos tarvitsee käydä tietorakennetta läpi rekursiivisesti, voidaan käyttää tarkasteluoperaatiota yhdessä Y-kombinaattorin kanssa
- tarvitsemme määritelmän muotoa: xxx 0 = … ja xxx (succ p) = … xxx p …
- λ-kalkyylissa: xxx = Y (λ i n. n (λ p. … (i p) …) …)
- esim. double = Y (λ i n. n (λ p. succ (succ (i p))) 0)

Muista: list ::= nil | cell element list
- nil =(def) λ n c. n
- cell =(def) λ e r. λ n c. c e r
määritetään summa erikseen molemmille muodostimille
- tyhjälle listalle summa on nolla
- ei-tyhjälle se riippuu jotenkin listan elementistä ja loppulistasta
- runko: sum = (λ l. l [tyhjän-listan-tapaus] (λ e r. [ei-tyhjän-tapaus]))

listan loppuosa on lista, siispä tehdään rekursiivinen kutsu
rekursiivinen määritelmä tehdään siten, että Y antaa funktion sille itselleen argumentiksi (kutsutaan tässä nimellä i)
- runko: sum = Y (λ i l. l [tyhjän-listan-tapaus] (λ e r. … (i r) …))
- käytettävissä on yksi elementti ja listan loppuosan summa
- tarvitsee vain miettiä, mikä on koko listan summan suhde listan loppuosan summaan
lopputulos: sum =(def) Y (λ i l. l 0 (λ e r. plus e (i r)))

Muista: nat = zero | succ nat
- zero =(def) λ s z. z
- succ =(def) λ n. λ s z. s n
- runko: compare = λ n m. n (λ p. [tapaus-n-ei-0]) [tapaus-n-0]
määritellään kaikille kahden luvun muodostimien yhdistelmille. Halutaan seuraavat ominaisuudet:
- jos n = 0 ja m = 0, yhtäsuuret; jos vain n = 0, n pienempi; jos vain m = 0, n suurempi
- muussa tapauksessa käsitellään lukujen edeltäjiä
- tässä tapauksessa suhde on erityisen suoraviivainen: n < m joss pred n < pred m

Halutaan siis compare, joka täyttää ehdot:
- compare 0 0 = eq
- compare (succ pn) 0 = gt
- compare 0 (succ pm) = lt
- compare (succ pn) (succ pm) = compare pn pm
- runko: compare = Y (λ i n m. n (λ pn. m (λ pn. … (i pn pm)) [tapaus-vain-m-0]) (m (λ pm. [tapaus-vain-n-0]) [tapaus-molemmat-0]))
jottei tarvisi määritellä vakioita eq, lt, gt, ne annetaan syötteeksi (eli käyttäjä määrittelee ne)
lopputulos: compare =(def) Y (λ i n m lt eq gt.
n (λ pn. m (λ pm. i pn pm lt eq gt) gt) (m (λ p. lt) eq))

Muista: nat = zero | succ nat
- zero =(def) λ s z. z
- succ =(def) λ n. λ s z. s n
yleinen elementtien poiminta
- yleistetty aiemmista määritelmistä first, second jne.
  - käytetään sekä listojen että numeroiden tarkastelua
- halutaan elem, jolla seuraavat ominaisuudet:
  - elem 0 (cell e r) = e
  - elem (succ p) (cell e r) = elem p r
- runko: elem = (λ n l. l Ω (λ e r. n (λ p. [tapaus-n-ei-0]) [tapaus-n-0]))
- elem =(def) Y (λ i n l. l Ω (λ e r. n (λ p. (i p r)) e)

Taas kerran rekursio numeroiden rakenteen perusteella
- Halutaan replace-elem, jolla seuraavat ominaisuudet:
  - replace-elem e 0 (cell e' r) = cell e r
  - replace-elem e (succ p) (cell e' r) = cell e' (replace-elem e p r)
- runko: replace-elem = Y (λ i n l. l Ω (λ e r. n (λ p. [tapaus-n-ei-0]) [tapaus-n-0]))
replace-elem =(def) Y (λ i e n l.
l Ω (λ e' r. n (λ p. (cell e' (i e p r))) (cell e r))

määrittely
- append nil l = l
- append (cell e r) l = cell e (append r l)
- append =(def) Y (λ i l1 l2. l1 l2 (λ e r. cell e (i r l2)))
yhtäläisyys lukujen yhteenlaskun kanssa ei ole sattuma
- plus = Y (λ i n m. n (λ p. succ (i p m)) m)
- valitettavasti muodostimemme on määritelty niin, että lukujen ja listojen tyhjä muodostin (zero / nil) käsitellään eri haarassa :(
luvut ovat ikään kuin listoja ilman elementtejä
- nat ::= zero | succ nat
- list ::= nil | cell element list