Szintaxisfák redukció utáni méretére vonatkozó becslés a típusos lambda kalkulusban
A lambda kalkulus konstansok nélküli változatának Exp nyelve az Exp ::= Var | (λVar.Exp) | (ExpExp) rekurzív definícióval értelmezett. Ehhez társítjuk az egyszerű típusokat, amelyek rekurzív definíciója: Typ ::= At | (Typ→Typ). A két nyelv felett értelmezhető a Γ⊦M:A („az M kifejezés típusa a Γ kontextusban az A”) háromváltozós reláció, ahol M egy Exp-beli kifejezés, A egy Typ-beli típus, Γ pedig olyan függvény, amely véges sok Var-beli változóhoz rendel Typ-beli típust. Ez a reláció tehát kapcsolatot teremt Exp és Typ között oly módon, hogy bizonyos Exp-beli kifejezésekhez Typ-beli típust rendel (feltéve, hogy a kifejezésbeli szabad változók típusa Γ-ban deklarálva van). Ezt a kalkulust nevezzük egyszerű típusos lambda kalkulusnak (STLC). [1]
Közismert tény, hogy az STLC-ben a beta-redukció, ami a (λx.M)N→M[x/N] cserét jelenti (ahol [x/…] a változó helyére való helyettesítés) minden esetben, véges sokszori alkalmazással, előbb-utóbb olyan kifejezést eredményez, ami már nem tartalmaz (λx.M)N alakú, úgy nevezett beta-redexet (ezek a normál kifejezések). [2] A redukciós eljárás az STLC-ban a legbonyolultabb redexek (a maximális redexek) redukálásával kezdődik, ahol a bonyolultságot az méri, hogy a (λx.M)N redex típusa hány → szimbólumot tartalmaz. A redukciós algoritmus bonyolultságát magát pedig az jellemzi, hogy a kifejezés szintaxisfája az eljárás közben mennyit nő. Fortune et al. bizonyította, hogy a normál kifejezések szintaxisfáinak magassága az eredeti fa magasságának hiperexponenciális függvényével becsülhető felül. [3] A dolgozatban ezt a bizonyítást vesszük szemügyre. Elsőként megállapítjuk, hogy a szintaxisfa méretére vonatkozó indukció helyett egy kétparaméteres, omega^2-ig menő transzfinit indukció is sikerre vezet. Másfelől, és ez az érdekesebb, ezt a bizonyítást úgy tudjuk módosítani, hogy rendes teljes indukciós bizonyítássá váljon, amennyiben a maximális redexek helyzetére vonatkozóan megszorításokat teszünk. Igazolni fogjuk, hogy ha adott n természetes számra azon Exp-beli kifejezésekre szorítkozunk, amelyekben a maximális redexek egymásba skatulyázott sorozatai nem hosszabbak mint n és a maximális redexek nincsenek magasabban, a szintaxisfában, mint n, akkor az normál kifejezések mérete az eredeti méret polinomiális (sőt: szuperlineáris) függvényénél nem nő erősebben.
Irodalom:
1. A. S. Troelstra, H. Schwichtenberg: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2000.
2. M. H. Sørensen, P. Urzyczyn: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, Volume 149. Elsevier Science, 2006.
3. Steven Fortune--Daniel Leivant--Michael O'Donnell: The Expressiveness of Simple and Second-Order Type Structures. Journal of the ACM, Vol. 30, Issue 1, pp. 151-185., 1983.
szerző
-
Mezei Szabolcs
Alkalmazott matematikus mesterképzési szak (MSc)
mesterképzés (MA/MSc)
konzulens
-
Dr. Molnár Zoltán Gábor
adjunktus, Algebra Tanszék
