Mikä on WikiWiki?
nettipäiväkirja
koko wiki (etsi)
viime muutokset
(Hahaa, otin käyttöön tämän termin ennen kuin m$ lanseerasi sen!)
Ohjelmointikieli, jossa tietotyypit sisältävät tiedon siitä, miten niiden (ekstensionaalinen) arvo määrittyy. Tämä edellyttää symbolimanipulaatiota, sillä arvon määritykset ovat symbolisarjoja ("ilmauksia"). Monimutkaisemmat ilmaukset edelleen säilyttäisivät kaiken tiedon siitä, kuinka ilmaus on muodostettu. Varsinainen evaluaatio olisi matemaattisen sieventämisen kaltaista.
Tämä on käytännössä teoreemantodistusjärjestelmä. Jos kieltäytyy käyttämästä yhtäkään ekstensiota, sitä lienee mahdotonta tehdä edes Turing-vastaavaksi. Idis on siis siinä, että ekstensiot eivät ole first-class; vain intensioihin voi viitata muuttujilla jne.
Esimerkki: derivointi intensionaalisesti ja ekstensionaalisesti:
x=5 d(3x^2) / dx = 3 d(x^2) / dx = 3 2x = 6x = 30 d(3x^2) / dx = (3(x+dx)^2 - 3x^2) / dx = (olkoon dx=x/100) (3 * 5.05^2 - 3*5^2) / 0.05 = (3 * 25.5025 - 3*25) / 0.05 = (76.5075 - 75) / 0.05 = 1.5075 / 0.05 = 30.15
Okei, tulos ei tällä kertaa ole edes sama; lähinnä pointti on siinä, että jos esim. funktio \x->3x^2 on ekstensionaalinen (sitä voi kutsua mutta ei destrukturoida), sitä ei edes kykene derivoimaan intensionaalisesti.
Intensionaalinen ohjelmointikieli olisi periaatteessa hyvin ilmaisuvoimainen: esimerkiksi, jos meillä olisi kielen primitiivinä (tai aiemmin määritettynä) kokonaislukujen joukko N, alkulukujen joukon voisi määrittää yksinkertaisesti:
alkuluvut = { xeN | AyeN AzeN (y<x & z<x & y>1 & z>1 => ! x=y*z) }
Toteutuksen pitäisi kyetä automaattisesti tekemään todistuksia, kuten esimerkiksi tämän sievennyksen:
{ xeN | x mod 2 = 0 } U { xeN | x mod 2 = 1 } ---> N
En ole edes ihan varma, riittääkö logiikka kuvausvoimaltaan vai tarvitaanko lisäksi esim. rekursiivisia määrittelyitä:
N = 0 U { x | EyeN (x=succ(y)) }
Eikä minulla ole aavistustakaan, miten tällaista pystyttäisiin käsittelemään automaattisissa todistuksissa; miten esimerkiksi tuon määrittelyn perusteella voisi tehdä seuraavan sievennyksen:
{ xeN | AyeN (x>y) } ---> {}