A fixpont izomorfizmus extrakciója a Lambek-lemma gépi bizonyításából
A kategóriaelméletben az F-algebra fogalma közös alapot nyújt az induktív adattípus vagy -- matematikai szóhasználattal -- az algebrai struktúra szintaxisának komputációsan értelmes (konstruktív) definíciójához. Egy tetszőleges endofunktor az induktív típus elemeit legyártó konstruktorrendszert illetve az algebra szignatúráját reprezentálja. Az F endofunktor esetén egy F-algebra egy (X,c) pár, amelyben X a kategória egy objektuma, c pedig egy F(X)->X morfizmus. Ekkor az induktív adattípus (vagy az algebrai struktúra szintaxisa) definíció szerint az iniciális objektum lesz az F-algebrák kategóriájában. Akár az induktívan definiált adattípust, akár a szabad algebrát mint szintaxist tekintjük, kiváló intuíciót biztosít a fogalom kategorikus szemantikájának megértéséhez az a tény, hogy a szóban forgó iniciális objektum az F endofunktornak fixpontja. Ezt mondja ki az úgy nevezett Lambek-lemma. (A fixponttulajdonság miatt az iniciális objektum valóban azt a struktúrát adja, ami generálja az összes szintaktikai elemet és csakis azokat.) A dolgozatban a szükséges fogalmi hátteret formalizáltuk a Coq nevű félautomatikus bizonyítóban, majd a Lambek-lemma és a további praktikusan választott segédtételek bizonyítását programoztam le. A kategória fogalmának definíciójában a konstruktivitás érdekében ezúttal a morfizmusok egyenlőségét is szerepeltetni kell, ezért a számítást a morfizmusok halmazainak úgy nevezett ,,szetoid poklában'' kellett végeznem (`Setoid Hell'). A fixponttulajdonságot kimondó számítógépes bizonyítás így nem pusztán egy konstrukció helyességét igazolja, hanem a levezetés maga gyártja le a szavatoltan helyes izomorfizmust, amit (ill. az inverzét) a felhasználó bármikor extraktálhat a bizonyításból. Erre a formalizált kategorikus szemantikára példákat is adok.
szerző
-
Baráth László
Villamosmérnöki szak, alapképzés
alapképzés (BA/BSc)
konzulens
-
Dr. Molnár Zoltán Gábor
adjunktus, Algebra Tanszék
