Kombinatorisk logik

Kombinatorisk logik är en gren av matematisk logik som behandlar grundläggande (det vill säga inte i behov av förklaring och inte analyserade) begrepp och metoder för formella logiska system eller kalkyler [1] [2] . Inom diskret matematik är kombinatorisk logik nära besläktad med lambdakalkyl , eftersom den beskriver beräkningsprocesser.

Sedan starten har kombinatorisk logik och lambdakalkyl klassificerats som icke-klassisk logik . Poängen är att kombinatorisk logik uppstod på 1920-talet, och lambdakalkyl på 1940-talet som en gren av metamatematiken med ett ganska väldefinierat syfte – att ge matematiken grund. Detta innebär att man efter att ha konstruerat den erforderliga "tillämpade" matematiska teorin - ämnesteorin - som speglar processerna eller fenomenen i den verkliga yttre miljön, kan använda den "rena" metateorin som ett skal för att klargöra ämnesteorins möjligheter och egenskaper . Det visade sig också snart att båda dessa system kunde betraktas som programmeringsspråk (se även kombinatorisk programmering ).

Hittills har båda dessa språk inte bara blivit grunden för hela massan av forskning inom datavetenskap , utan används också i stor utsträckning inom programmeringsteori. Datorernas tillväxt av datorkraft har lett till automatisering av en betydande del av teoretiska (logiska och matematiska) kunskaper, och kombinatorisk logik, tillsammans med lambdakalkyl, anses vara grunden för resonemang i termer av objekt. .

Grundläggande begrepp

I kombinatorisk logik är de grundläggande begreppen en enplatsfunktion och operationen att applicera en funktion på ett argument ( applikation ). Begreppet funktion tas som primärt i förhållande till begreppet en mängd . En funktion förstås generiskt och kan verka på objekt på samma nivå som argument och värden. Eftersom argumentet för en funktion kan vara en funktion, kan en flerplatsfunktion reduceras till en enplatsfunktion [3] .

En kombinator är en funktion som uppfyller jämställdheten $f$

fg_{1}g_{2}\dots g_{n}=(\dots ((fg_{1})g_{2})\dots g_{n})=X,

där ( ) är några funktioner, X är ett objekt konstruerat från funktioner som använder applikation [3] . $g_1, g_2, \dots, g_n$ $n\geqslant 1$

Alla kombinatorer kan uttryckas i termer av två kombinatorer S och K definierade av följande likheter [3] :

Sxyz=xz(yz)

( distributör ),

kxy=x

( anfallare ).

Med ett lambdauttryck kan du alltid bygga ett applikativt uttryck . Detta kräver bara två kombinatorer: S och K . I form av lambda-uttryck: , . Det vill säga, den kombinatoriska logiken som definieras på dessa kombinatoriska objekt kan betraktas som en modell av lambdakalkylen [4] . $K = \lambda x.\lambda yx$ $S=\lambda f.\lambda g.\lambda x.fx(gx)$

Andra exempel på kombinatorer (i notationen av lambdakalkylen) är identitetsfunktionen , lätt uttryckt i termer av S och K [4] :

I = \lambda xx = SKK

och fixpunktskombinatorn eller Y-kombinatorn :

Y=\lambda h.((\lambda xh(xx))(\lambda xh(xx))).

Historik

År 1920 introducerades kombinatorer som speciella matematiska enheter [5] ursprungligen av M. Sheinfinkel [6] . Några år senare återupptäcktes de självständigt av H. Curry [7] , som sedan dess har gjort stora framsteg inom kombinatorisk logik (även om andra forskare, som Rosser, också har bidragit till detta arbete vid olika tidpunkter). Nästan samtidigt började Church , Rosser och Kleene utvecklingen av λ-omvandlingen.

Sedan 1970-talet har kombinatorer använts på tre huvudsakliga sätt: för det första för att bygga logiska system baserade på en abstrakt notation av en operation; för det andra i bevisteorin som grund för registrering av konstruktiva funktioner av olika slag; för det tredje, i konstruktion och analys av vissa programmeringsspråk inom datavetenskap .

Kategorisk kombinatorisk logik

Inom ramen för kombinatorisk logik byggs en speciell version av beräkningsteorin, kallad den kategoriska abstrakta maskinen . För detta introduceras ett speciellt fragment av kombinatorisk logik i beaktande - kategorisk kombinatorisk logik [8] . Den representeras av en uppsättning kombinatorer, som var och en har ett oberoende värde som en instruktion för ett programmeringssystem. Således är ytterligare en användbar applikation inbyggd i kombinatorisk logik - ett programmeringssystem baserat på en kartesisk sluten kategori (fc). Detta gör att du kan tänka om sambandet mellan operatören och den applicerade programmeringsstilen igen på en ny nivå.

Illativ kombinatorisk logik

Genom att använda begreppet objekt som abstrakta matematiska enheter med vissa substitutionsegenskaper är det möjligt att bygga system av logiskt resonemang . Det mest kända bland sådana system är baserat på kombinatorer.

Logik baserad på kombinatorer, eller illativ kombinatorisk logik , är byggd från teorin om kombinatorer eller lambda-kalkyl, utökad med ytterligare konstanter - extra konstanter - tillsammans med motsvarande axiom och inferensregler, som ger ett medel för deduktiv slutledning.

Se även

Anteckningar

↑ Ed. F. V. Konstantinova. Kombinatorisk logik // Philosophical Encyclopedia: i 5 volymer . - M . : Sovjetiskt uppslagsverk, 1960-1970.
↑ Kondakov, 1971 .
↑ 1 2 3 MES, 1988 , sid. 275-276.
↑ 1 2 Field, Harrison, 1993 , sid. 291-293.
↑ Cardone F., Hindley J. R. History of lambda calculus and combinators ( arkiverad 10 oktober 2011 på Wayback Machine ), i Handbook of the History of Logic, volym 5, DM Gabbay och J. Woods (red) (Amsterdam: Elsevier Co. ., att framträda).
↑ Schonfinkel M. Uber die Baustein der mathematischen Logik. — Matematik. Annalen, vol. 92, 1924, sid. 305-316.
↑ Curry H. B. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509-536, 789-834, 1930.
↑ Curien P.-L. Kategorisk kombinatorisk logik. — LNCS, 194, 1985, sid. 139-151.

Litteratur

Wolfenhagen VE Kombinatorisk logik i programmering. Beräkningar med objekt i exempel och problem. - 2:a uppl. - M . : AO Center YurInfoR, 2003. - 204 sid. — ISBN 5-89158-101-9 .
Kondakov N. I. Logisk ordbok / Gorsky D. P. - M . : Nauka, 1971. - 656 sid.
Fält A., Harrison P. Funktionell programmering = Funktionell programmering. — M .: Mir, 1993. — 637 sid. — ISBN 5-03-001870-0 .
Mathematical Encyclopedic Dictionary / Yu. V. Prokhorov. - M . : Soviet Encyclopedia, 1988. - 847 sid.
A.S. Kuzichev. Kombinatorisk logik // New Philosophical Encyclopedia : i 4 volymer / föregående. vetenskaplig-ed. råd av V. S. Stepin . — 2:a uppl., rättad. och ytterligare - M . : Tanke , 2010. - 2816 sid.

Ordböcker och uppslagsverk	Stor ryss
I bibliografiska kataloger	BNF : 119473722 GND : 4164750-6 J9U : 987007543265905171 LCCN : sh85028814 SUDOC : 027430677