Kategorisk abstrakt maskine

Den kategoriske abstrakte maskine (CAM) er en programberegningsmodel [1] , som bevarer funktionerne i den applikative, funktionelle eller kompositoriske stil. Den er afhængig af teknikken til applikativ beregning .

En tilgang til implementering af funktionelle sprog er givet af den superkombinator -baserede maskine eller David Turners SK-maskine . Forestillingen om en kategorisk abstrakt maskine giver en alternativ tilgang[ angiv ] . Strukturen af ​​QAM omfatter syntaktiske, semantiske og beregningsmæssige bestanddele[ angiv ] . Syntaksen er baseret på de Bruijn-formalismen, hvis brug overvinder vanskelighederne forårsaget af brugen af ​​bundne variable. Semantik ligner i sine udtryksmuligheder SK-maskinen. Beregningerne udføres på en måde svarende til dem, der bruges i Landins SECD- maskine . At tage sådanne holdninger[ klargør ] Det kategoriske abstrakt giver konsistente grundlag for syntaks, semantik og beregningsteori. En sådan integration sker ikke uden indflydelse af funktionel programmeringsstil.

Begrebet en kategorisk abstrakt maskine opstod i midten af ​​1980'erne og spiller rollen som en variant af teorien om beregning for programmører.[ angiv ] . Fra et teoretisk synspunkt er en kategorisk abstrakt maskine repræsenteret af en kartesisk lukket kategori og er nedsænket i kombinatorisk logik . Maskininstruktioner er kombinatorobjekter, der tilsammen danner en speciel variant af kombinatorisk logik - kategorisk kombinatorisk logik. Den kategoriske abstrakte maskine er en klar og matematisk korrekt repræsentation af funktionelle programmeringssprog. Ved hjælp af lige udtryk kan maskinkode optimeres . Særligt tydelige er de forskellige beregningsmekanismer - rekursion , doven evaluering , - samt mekanismerne til at videregive parametre - kalde ved navn, kalde efter værdi osv. Fra et teoretisk synspunkt bevarer en kategorisk abstrakt maskine alle fordelene ved en objektorienteret tilgang til programmering .

De Bruijns formalisme

De Bruijn- formalismen er en teknik til at omdøbe bundne variable ( formelle parametre ), som giver dig mulighed for at undgå bindingskollisioner, når du udskifter formelle parametre med faktiske. Det bruges ved kompilering af programkode på KAM. Denne omdøbningsteknik kaldes også de Bruijn-kodning , og den tillader faktisk, at apparatet til λ-regningen kan bruges på samme rettigheder som apparatet for kombinatorisk logik .

Se også

Noter

  1. Cousineau G., Curien P.-L., Mauny M. Den kategoriske abstrakte maskine. — LNCS, 201, Funktionelle programmeringssprog computerarkitektur.-- 1985, s.~50-64.

Litteratur