Tässä luennossa

• Jipii jipii, mikä uudelleenkirjoitusjärjestelmä! Ai niin, mitä sillä siis tehtiinkään?
• Esimerkkejä lambdalausekkeiden redusoinnista
• Funktioiden olemuksesta (ja toki toiminnastakin)
• Useamman argumentin funktiot ja osittaissovellus
• Lisää esimerkkejä lambdalausekkeista

HIENO! Mitä sillä voi tehdä?

• uudelleenkirjoitusjärjestelmien merkityksestä
  • esimerkkejä
• lambdakalkyylin merkitys

Uudelleenkirjoitusjärjestelmien merkityksestä

• uudelleenkirjoitusjärjestelmillä (kuten β-reduktioon perustuvalla lambdakalkyylilla) pystyy tekemään vaikka mitä
  • siinä mielessä, että yksinkertaisetkin uudelleenkirjoitusjärjestelmät voivat toimia tosi mielenkiintoisin tavoin
• hieno juttu, mutta joskus merkitys unohtuu…
• on vaikeaa tutkia uudelleenkirjoitusjärjestelmän muodollisiakaan ominaisuuksia, jos ei ole mitään hajua siitä, millaisia ilmiöitä järjestelmä kuvaa
• tutustutaan siis lambdakalkyylin semantiikkaan.

Erilaiset uudelleenkirjoitusjärjestelmät mallintavat yleensä erilaisia ilmiöitä (muuten niissä ei ole niin paljon pointtia).

• aritmetiikka mallintaa laskettavissa olevien asioiden ryhmien käyttäytymistä
  • esim. 3 + 5 => 8 mallintaa sitä, että jos lämää kaksi papukasaa yhteen, niistä tulee tietyn kokoinen kasa
• logiikka mallintaa tosiasioiden suhteita
  • esim. (otat → et aja), otat => et aja mallintaa sitä, että sovelletaan ehdollista päättelyä faktoihin
• mitä mallintaa lambdakalkyyli?

Lambdakalkyylin merkitys

• lambdakalkyyli mallintaa pelkistetyssä muodossa, mitä on aineiston käsittely
• jokainen abstraktio kuvaa aineistoa tietyllä lailla käsittelevää konetta / funktiota
• (λ x. e) on kone, joka ottaa syötteeksi jonkin aineiston x, ja tuottaa siitä tuloksen e
• jokainen applikaatio (sovellus) kuvaa koneen käynnistämistä
• (e1 e2) on käynnistys, jossa koneelle e1 annetaan aineistoksi kone e2 (ja e1:n tulos korvaa sitten tämän lausekkeen)
• alkuun epäintuitiivista, koska lambdakalkyylissa aineistot ovat myös koneita…

Ruksutiruks, lambdalausekkeiden toimintaa

• esimerkkejä lambdalausekkeiden merkityksistä
  • ja niiden evaluointia
• interlude: nimien käyttö
• syötettään kutsuvat funktiot (syötteensä käynnistävät koneet)

Esimerkkejä lambdalausekkeiden merkityksestä

• (λ a. a) on kone, joka ottaa aineiston ja jonka tuloksena on sama aineisto muuntumattomana
• helppo nähdä: syöte (a) ja tulos (a) ovat samoja
• kutsutaan myös identiteettifunktioksi
• (λ a. (λ b. b)) on kone, joka ottaa aineiston muttei käytä sitä mihinkään vaan tuloksena on aina identiteettifunktio
• tällaisia syötteensä roskiin heittäviä koneita sanotaan vakiofunktioiksi (koska niiden tulos on aina sama)
• katsotaanpa, mitä tapahtuu, kun ne käynnistetään…

Koneiden käynnistäminen

• (λ a. a) (c (d e) f) → (c (d e) f)
• Jee! Identiteettifunktio tosiaan palautti syötteen sellaisenaan
• (λ a. (λ b. b)) (c (d e) f) → (λ b. b)
• (λ a. (λ b. b)) (g (e f)) → (λ b. b)
• Tuplajee! Vakiofunktion tulos tosiaan on vakio
• tähän mennessä aika helppoa, koska lambdalausekkeemme eivät tee syötteellään mitään monimutkaista, nimittäin käynnistä sen kuvaamaa konetta.

Nimien käytöstä

• abstraktio on siis tietynlainen funktio (funktio ohjelmointimielessä)
• yleensä ohjelmointikielissä funktiot määritellään nimeltä ja käytetään nimellä
• esim. int ident(int x) { return x; } ja sitten ident(3)
• lambdakalkyylissa: (λ x. x) 3
• lambdakalkyylissakin käytetään usein nimiä ihmisten ymmärtämisapuna
• esim. ident = (λ x. x) ja sitten ident 3

Syötteensä käynnistävät koneet

• syötteen käynnistäminen on lambdakalkyylissa ainoa tapa tehdä jotain syötteen perusteella
• oliokielellä: jokainen arvo on läpinäkymätön tietotyyppi, jolla on tasan yksi virtuaalimetodi

(λ a. a a)

• käynnistää syötteensä antaen sen sille itselleen argumentiksi
• (λ a. a a) (λ b. b) => (λ b. b) (λ b. b) => (λ b. b)
• (λ a. a a) (λ b. b b) => (λ b. b b) (λ b. b b) => …

Tietotyyppien mallintaminen

• ensimmäinen esimerkki tietotyypistä: bitti
  • paitsi ei vielä, vaan ensin…
• kaksi- ja useampiargumenttisten funktioiden rakentaminen
  • esimerkkinä yhteenlasku
• bittien määrittely
• loogiset konnektiivit

Ensimmäinen esimerkki tietotyypistä: bitti!

• oikeasti totuusarvo tai valinta (joo / ei, vasen / oikea)
• mallinnetaan 2-argumenttisella funktiolla: tosi =(def) funktio, joka palauttaa 1. argumenttinsa, epätosi =(def) funktio, joka palauttaa 2. argumenttinsa.
• mutta hetkonen, lambdalausekkeessahan on aina vain yksi syöte…
• eli ensin pitää päättää, miten esitetään useampiargumenttiset funktiot

Kaksi- ja useampiargumenttisten funktioiden rakentaminen

• kaksiargumenttisen funktion voi mallintaa kahdella tavalla:
  • funktiona, joka ottaa syötteekseen parin
  • funktiona, joka ottaa yhden argumentin ja palauttaa funktion, joka ottaa toisen argumentin ja sitten palauttaa varsinaisen tuloksen.
• koska emme ole vielä määritelleet pareja, käytämme jälkemmäistä tapaa
• esimerkiksi (λ a. (λ b. b a)) on tulkinnallisesti kaksiargumenttinen funktio
  • ottaa argumentit a ja b ja palauttaa sen, mitä b palauttaa kun sille antaa syötteeksi a:n (b a)
• tämä on perustelu lyhennemerkinnälle (λ a b. b a)

Esimerkkinä yhteenlasku

• Oletetaan, että olemme määritelleet yhteenlaskun ja numerot uudelleenkirjoitussääntöinä
  • oikeasti ne voidaan mallintaa lambdalausekkeinakin, näemme tämän myöhemmin
• yhteenlaskufunktion voisi kirjoittaa lambdalausekkeena (λ a b. a + b)
• (λ a. (λ b. a + b)) 3 5 => (λ b. 3 + b) 5 => 3 + 5 (ooh!)
• sivuseurauksena on, että ((λ a b. a + b) 3) on funktio, nimittäin kolmenlisäysfunktio.
  • jostain mystisestä syystä Haskell-kielessä tätä kolmenlisäysfunktiota kutsutaan nimellä (3 +).

Takaisin bitteihin, määrittely

• true =(def) (λ a b. a)
• false =(def) (λ a b. b)
• if on funktio, joka ottaa syötteekseen totuusarvon ja kaksi lauseketta, joista se palauttaa ensimmäisen, jos oli tosi, ja toisen, jos oli epätosi
  • hyvin helppo määritellä: if =(def) (λ a b c. a b c) (joka puolestaan on η-säännöllä (λ a. a)
• muita esimerkkejä totuusarvojen käytöstä?

Loogiset konnektiivit

• not =(def) (λ a. if a false true) = (λ a. a false true)
  • helppo tajuta: jos a on tosi, tulos on epätosi ja päin vastoin
• and =(def) (λ a b. if a b false) = (λ a b. a b false)
  • vähän vaikeampi: jos a on tosi, tulos on b (???), muuten aina epätosi
• or =(def) (λ a b. if a true b) = (λ a b. a true b) = (λ a. a true)
  • samanlainen mutta lisäksi sieventyy η-reduktion vuoksi vaikeasti käsitettävään muotoon