Logica combinatorie

Logica combinatorie este o ramură a logicii matematice care se ocupă de concepte și metode fundamentale (adică nu au nevoie de explicație și nu sunt analizate) ale sistemelor logice formale sau calculelor [1] [2] . În matematica discretă , logica combinatorie este strâns legată de calculul lambda , deoarece descrie procesele de calcul.

De la începuturile lor, logica combinatorie și calculul lambda au fost clasificate ca logici neclasice . Ideea este că logica combinatorie a apărut în anii 1920, iar calculul lambda în anii 1940 ca o ramură a metamatematicii cu un scop destul de bine definit - de a da baze matematicii. Aceasta înseamnă că, după ce a construit teoria matematică „aplicată” necesară – teoria subiectului – care reflectă procesele sau fenomenele din mediul extern real, se poate folosi metateoria „pură” ca înveliș pentru a clarifica posibilitățile și proprietățile teoriei subiectului. . De asemenea, s-a dovedit curând că ambele sisteme ar putea fi considerate limbaje de programare (vezi și programarea combinatorie ).

Până în prezent, ambele limbaje au devenit nu numai baza pentru întreaga masă de cercetare în domeniul informaticii , ci sunt și utilizate pe scară largă în teoria programării. Creșterea puterii de calcul a computerelor a condus la automatizarea unei părți semnificative a cunoștințelor teoretice (logice și matematice), iar logica combinatorie, împreună cu calculul lambda, este recunoscută ca bază pentru raționament în termeni de obiecte. .

Concepte de bază

În logica combinatorie, conceptele de bază sunt o funcție unică și operația de aplicare a unei funcții la un argument ( aplicație ). Conceptul de funcție este considerat primar în raport cu conceptul de mulțime . O funcție este înțeleasă într-un mod general și poate opera cu obiecte de același nivel cu argumentele și valorile. Deoarece argumentul unei funcții poate fi o funcție, o funcție cu mai multe locuri poate fi redusă la o funcție cu un singur loc [3] .

Un combinator este o funcție care satisface egalitatea $f$

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

unde ( ) sunt unele funcții, X este un obiect construit din funcții folosind aplicația [3] . $g_1, g_2, \dots, g_n$ $n\geqslant 1$

Orice combinator poate fi exprimat în termenii a doi combinatori S și K definiti prin următoarele egalități [3] :

Sxyz=xz(yz)

( distribuitor ),

kxy=x

( atacant ).

Având în vedere o expresie lambda, puteți construi oricând o expresie aplicativă . Acest lucru necesită doar două combinatoare: S și K . Sub formă de expresii lambda: , . Adică, logica combinatorie definită pe aceste obiecte combinatorii poate fi considerată ca un model al calculului lambda [4] . $K = \lambda x.\lambda yx$ $S=\lambda f.\lambda g.\lambda x.fx(gx)$

Alte exemple de combinatoare (în notația calculului lambda) sunt funcția de identitate , ușor de exprimat în termeni de S și K [4] :

I = \lambda xx = SKK

și combinatorul în virgulă fixă sau combinatorul Y :

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

Istorie

În 1920, combinatorii ca entități matematice speciale [5] au fost introduși inițial de M. Sheinfinkel [6] . Câțiva ani mai târziu, ele au fost redescoperite în mod independent de H. Curry [7] , care de atunci a făcut progrese majore în logica combinatorie (deși alți cercetători, precum Rosser, au contribuit și ei la această lucrare în diferite momente). Aproape în același timp, Church , Rosser și Kleene au început dezvoltarea conversiei λ.

Din anii 1970, combinatoarele au fost folosite în trei moduri principale: în primul rând, pentru a construi sisteme logice bazate pe o notație abstractă a unei operații; în al doilea rând, în teoria dovezilor ca bază pentru înregistrarea funcţiilor constructive de diferite tipuri; în al treilea rând, în construirea și analiza unor limbaje de programare în informatică .

Logica combinatorie categorica

În cadrul logicii combinatorii, este construită o versiune specială a teoriei calculului, numită mașina abstractă categorică . Pentru aceasta, este introdus în considerare un fragment special de logica combinatorie - logica combinatorie categorică [8] . Este reprezentat de un set de combinatoare, fiecare având o valoare independentă ca instrucțiune a unui sistem de programare. Astfel, o altă aplicație utilă este încorporată în logica combinatorie - un sistem de programare bazat pe o categorie închisă carteziană (fc). Acest lucru vă permite să regândiți legătura dintre operator și stilul de programare aplicativă încă o dată la un nou nivel.

Logica combinatorie ilativă

Folosind conceptul de obiecte ca entități matematice abstracte cu anumite proprietăți de substituție, este posibil să se construiască sisteme de raționament logic . Cel mai faimos dintre astfel de sisteme se bazează pe combinatoare.

Logica bazată pe combinatori, sau logica combinatorie ilativă , este construită din teoria combinatorilor sau calculul lambda, extinsă prin constante suplimentare - constante suplimentare - împreună cu axiomele și regulile de inferență corespunzătoare, care oferă un mijloc de inferență deductivă.

Vezi și

Note

↑ Ed. F. V. Konstantinova. Logica combinatorie // Philosophical Encyclopedia: in 5 volumes . - M . : Enciclopedia Sovietică, 1960-1970.
↑ Kondakov, 1971 .
↑ 1 2 3 MES, 1988 , p. 275-276.
↑ 1 2 Field, Harrison, 1993 , p. 291-293.
↑ Cardone F., Hindley J. R. History of lambda calculus and combinators ( Arhivat 10 octombrie 2011 la Wayback Machine ), în Handbook of the History of Logic, Volumul 5, DM Gabbay și J. Woods (eds) (Amsterdam: Elsevier Co ., a aparea).
↑ Schonfinkel M. Uber die Baustein der mathematischen Logik. — Matematică. Annalen, voi. 92, 1924, p. 305-316.
↑ Curry H. B. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509-536, 789-834, 1930.
↑ Curien P.-L. Logica combinatorie categorica. — LNCS, 194, 1985, p. 139-151.

Literatură

Wolfenhagen VE Logica combinatorie în programare. Calcule cu obiecte în exemple și probleme. - Ed. a II-a - M . : AO Center YurInfoR, 2003. - 204 p. — ISBN 5-89158-101-9 .
Kondakov N. I. Dicționar logic / Gorsky D. P. - M . : Nauka, 1971. - 656 p.
Câmpul A., Harrison P. Programare funcțională = Programare funcțională. — M .: Mir, 1993. — 637 p. — ISBN 5-03-001870-0 .
Dicţionar enciclopedic matematic / Yu. V. Prokhorov. - M . : Enciclopedia Sovietică, 1988. - 847 p.
A. S. Kuzicev. Logica combinatorie // New Philosophical Encyclopedia : în 4 volume / prev. științific-ed. sfatul lui V. S. Stepin . — Ed. a II-a, corectată. si suplimentare - M . : Gândirea , 2010. - 2816 p.

Dicționare și enciclopedii	Rusă mare
În cataloagele bibliografice	BNF : 119473722 GND : 4164750-6 J9U : 987007543265905171 LCCN : sh85028814 SUDOC : 027430677