Structure and Interpretation of Computer Programs
16 April 2008 (books programming ISC)Az egyik dolog, amit nagyon szeretek a progmaton a Simon-féle analízis kurzusban, az az, ahogyan gyakorlatilag a semmiből, vagyis a ZF-ből és a valós számok axiómáiból építkezünk, és ha néha ki is hagyunk egy-egy bizonyítást, akkor arra külön fel van hívva a figyelmünk. Ennek az a csodálatos eredménye, hogy még így a hatodik félév közepén is bármilyen bonyolult tétel bizonyítása esetén elvileg rekonstruálható a teljes út az axiómáktól.
A SICP, mint alant kifejtem, ugyanilyen előadássorozat illetve könyv, a programozásról. Én egy-két évvel ezelőtt először az előadással találkoztam, ma már nem tudom, miért hagytam abba akkoriban a 6. előadás környékén. Most viszont elémkerült a könyv is, nekiugrottam, és kiderült, hogy a lényeg pont a második felében van.
Az első három fejezet ugyanis bármelyik, hasonló témájú könyvben
előfordulna: az absztrakció különböző, egymásra épülő vagy éppen
ortogonális szintjei, mint pl. (magasabbrendű) függvények,
adatok és műveleteik együttes kezelése (hadd ne mondjam
típus), az imperatív megközelítés a maga
értékadásos-mellékhatásos fekélyeivel, Haskell-szerű lazy
evaluáció. Az összes illusztráció Scheme-ben,
egy Lisp dialektusban íródott, valójában az első három fejezet
éppen arról szól, ahogyan a fenti absztrakciós eszközök
céljainak megvizsgálásával felépül a nyelv szemantikája.
Az érdekességek a negyedik fejezetben kezdődnek. Először, egyfajta baseline-ként bemutat egy Scheme-ben írt Scheme interpretert, ennek ugye Lispben eleve komoly hagyományai vannak (összehasonlíthatatlanul olvashatóbb a mai szemnek ugyanennek a cikknek a Paul Graham által felújított változata). Ezzel már sokkal valóságosabbá válnak az eddigi programok, hiszen bár a kígyó még a saját farkába harap, de már kezünkben van az axiómáknak az a véges halmaza, amikből a konkrét Scheme programok szemantikája levezethető.
Ezekután bemutatja a Scheme pár leágazását, és persze hogy itt
válik érdekeltté az intencionális programozó. A
Lispben ugye régóta kultúrája van annak, hogy a problémákat a
hozzájuk illesztett nyelven oldjuk meg, és utána vagy írjuk meg
ennek a nyelvnek az értelmezését, vagy ágyazzuk be a nyelvet a
Lispbe. Így aztán a tipikus Lisp programozó a legritkább esetben
programozik Lispben, sokkal gyakrabban mindenféle ad-hoc Lisp'
meg Lisp'' nyelvekben. A negyedik fejezet ilyen Scheme'
nyelveket mutat be a lazy evaluációhoz és a nemdeterminisztikus
futási szemantikához (ez utóbbi egyébként valószínűleg közel áll ahhoz,
ahogyan a kvantumszámítógépeket fogjuk magasszinten
programozni); illetve egy interpretált constraint-nyelvet.
És végül az utolsó fejezet az, ami odavág. Nem azért, mintha nem láttunk volna még a bootstrap-probléma megoldására gépi kódban írt compilert, hanem azért, ahogyan kerekké teszi a könyvet. Itt jön be ugyanis a korábban említett párhuzam az anal-kurzussal. Bebizonyítjuk, hogy létezik rendezett teljestest: a valódi, fizikai számítógépeket leíró regisztergép-modellen az utolsó bitig egyértelművé válik minden maradék kérdésre a válasz, a bemutatott, gépi kódú Scheme interpreter és fordító pedig hirtelen megfoghatóvá tesz minden, a könvyben megelőző példát. Handwaving-nek nyoma sem marad. Ahogy az utolsó előtti előadáson Abelson mondja: az utolsó, legnagyobb varázslat, hogy kiírtjuk a rendszerből a mágiát.