Logica della computabilità

La logica della computabilità (Computability logic o CoL) è un programma di ricerca e un modello matematico per riqualificare la logica come una teoria formale sistematica della computabilità, in contrapposizione alla logica classica che può essere vista come una teoria formale della verità. È stato presentata per la prima volta e così nominata da Giorgi Japaridze nel 2003^[1].

Se si confronta la CoL con la logica classica si potrebbe dire che, mentre nella seconda le formule rappresentano enunciati veri o falsi, nella CoL rappresentano problemi computazionali. Nella logica classica, la validità di una formula è intesa come "la formula è sempre vera", ossia indipendentemente dall'interpretazione delle sue sottoformule primitive (variabili extralogiche, cioè enunciati atomici). In modo simile, nella CoL validità significa essere sempre computabile. Più in generale, la logica classica ci dice quando la verità di un certo enunciato segue sempre dalla verità di un dato insieme di altri enunciati. Allo stesso modo, la CoL ci dice quando la computabilità di un certo problema A segue sempre dalla computabilità di altri problemi dati B₁, ...,B_n. Inoltre, la CoL fornisce un metodo uniforme per realizzare effettivamente una soluzione (algoritmo) di tale problema A da qualsiasi soluzione nota di B₁, ..., B_n.

La logica della computabilità interpreta i problemi computazionali nel loro senso più generale - interattivo. Questi, infatti, sono formalizzati come giochi giocati da una macchina contro il suo ambiente, e la computabilità significa l'esistenza di una macchina che vince il gioco contro qualsiasi possibile comportamento dell'ambiente. Definendo il significato di queste macchine-giocatori, la CoL fornisce una generalizzazione della Tesi di Church-Turing al livello della computazione interattiva, che è anche il tipo usuale di computazione dei computer reali (con diversi input e output). Il classico concetto di verità risulta così essere un caso speciale con interattività di grado zero della computabilità. Questo rende la logica classica un frammento particolare della CoL. Essendo un'estensione conservativa della logica classica, la logica della computabilità è, allo stesso tempo, di un ordine di grandezza più espressiva, costruttiva e computazionalmente significativa. Oltre alla logica classica, l'independence-friendly logic (IF) e alcune estensioni proprie della logica lineare e della logica intuizionista si rivelano essere, parimenti, frammenti naturali della logica della computabilità^[2][3]. Quindi concetti significativi di "verità intuizionista", "verità lineare" e "IF-verità" possono essere derivati dalla semantica della CoL.

Fornendo una risposta sistematica alla domanda fondamentale di ciò che può essere calcolato e come, CoL sostiene un'ampia gamma di potenziali aree applicative. Queste includono teorie costruttive applicate, knowledge base systems e sistemi di pianificazione e azione. Di questi, solo le applicazioni in teorie costruttive applicate sono state estesamente esplorate fino ad ora: sono state costruite una serie di teorie dei numeri basati sulla CoL, chiamate "clarithmetics"^[4][5], come alternative significative, dal punto di vista computazionale della teoria della complessità, dell'Aritmetica di Peano basata sulla logica classica e delle sue variazioni come i sistemi di aritmetica limitata.

I tradizionali sistemi formali di dimostrazione come la deduzione naturale o il calcolo dei sequenti risultano insufficienti per l'assiomatizzazione di frammenti più o meno non triviali della CoL. Ciò ha comportato lo sviluppo di metodi di prova alternativi, più generali e flessibili, come il calcolo dei circuenti^[6][7].

Il linguaggio completo della CoL è un'estensione del linguaggio della logica del primo ordine. Il suo vocabolario logico ha diversi tipi di congiunzioni, disgiunzioni, quantificatori, implicazioni, negazioni e cosiddetti operatori di ricorrenza. Questa collezione comprende tutti i connettivi e quantificatori della logica classica. Il linguaggio ha anche due tipi diversi di atomi non logici: elementari e generali. Gli atomi elementari, che non sono altro che le proposizioni atomiche della logica classica, rappresentano problemi elementari, ovvero giochi senza movimenti che vengono automaticamente vinti dalla macchina quando veri e perduti quando sono falsi, in modo assegnato a priori. D'altra parte, gli atomi generali possono essere interpretati come qualsiasi gioco, elementare o non elementare. Sia semanticamente che sintatticamente, la logica classica non è altro che il frammento della CoL ottenuto non permettendo atomi generali nel suo linguaggio così come proibendo tutti gli operatori (costanti logiche del linguaggio) diversi da ¬, ∧, ∨, →, ∀, ∃.

Japaridze ha ripetutamente sottolineato che il linguaggio del CoL è in fieri e potrebbe subire ulteriori estensioni. A causa dell'espressività di questo linguaggio, i singoli progressi e ricerche nel settore della CoL, come la costruzione di assiomatizzazioni o di teorie applicate basate su di essa, sono di solito limitati solo ad uno o a un altro frammento proprio del linguaggio.

I giochi alla base della semantica di CoL sono chiamati "giochi statici". Tali giochi non stabiliscono regole su quale giocatore possa o debba muoversi in una data situazione, e generalmente spetta al giocatore decidere se fare la propria mossa o attendere quelle del suo avversario. C'è sempre una possibilità che l'avversario faccia la sua mossa mentre l'altro giocatore sta "pensando" alla propria mossa successiva. Ciononostante i giochi statici sono definiti in modo tale che ritardare le proprie mosse non dannegga un giocatore in nessun caso, e perciò questi giochi non si trasformano mai in gare di velocità. Tutti i giochi elementari sono di per loro statici, e lo sono ugualmente i giochi che possono essere interpretazioni di "atomi generali". Nei giochi statici ci sono due giocatori: la macchina e lambiente. La macchina può seguire solo strategie algoritmiche, mentre non vi sono restrizioni sul comportamento dell'ambiente. Ogni partita viene vinta da un giocatore e persa dall'altro.

Gli operatori logici di CoL sono intesi come operazioni sui giochi. Esaminiamo ora informalmente alcune di queste operazioni. Per semplicità supponiamo che il dominio del discorso sia sempre {0,1,2,…}.

L'operazione ¬ di negazione ("non") inverte i ruoli dei due giocatori, scambiando l'ordine delle mosse e le vittorie della macchina in quelle dell'ambiente e viceversa. Per esempio, se Scacchi è il gioco degli scacchi (ma senza la possibilità del pareggio) dalla prospettiva del giocatore con i bianchi, allora ¬Scacchi è lo stesso gioco giocato dalla prospettiva del giocatore che usa i pezzi neri.

La congiunzione parallela ∧ ("pand") e la disgiunzione parallela ∨ ("por") combinano i giochi in modo parallelo. Una partita di A ∧ B o A ∨ B è un gioco simultaneo nei due congiunti. La macchina vince A ∧ B (risp. A ∨ B) se vince entrambi (risp. almeno uno) di quei giochi. Quindi, per esempio, Scacchi ∨ ¬Scacchi è un gioco su due scacchiere, uno giocato dalla macchina con i bianchi e l'altro con i neri dove il suo compito è quello di vincere in almeno un tavolo di gioco. Un gioco simile può essere facilmente vinto a prescindere da chi sia l'avversario copiando le sue mosse da un tavolo di gioco all'altro. L'operatore di implicazione parallela → ("pimplication") è definito da A → B = ¬A ∨ B. Il significato intuitivo di questa operazione è ridurre B a A, ossia che si è in grado di risolvere A finché l'avversario riesce a risolvere B. I quantificatori paralleli ∧ ("pall") e ∨ ("pexists") possono essere definiti con ∧xA(x) = A(0) ∧ A(1) ∧ A(2) ∧... e ∨xA(x) = A(0) ∨ A(1) ∨ A(2) ∨... . Queste sono quindi giocate simultanee di A(0), A(1), A(2),... ciascuna su un "ambiente di gioco" separato. La macchina vince ∧xA(x) (risp. ∨xA(x)) se vince tutti (risp. alcuni) di questi giochi. I quantificatori ciechi ∀ ("blall") e ∃ ("blexists"), d'altra parte, generano giochi "singoli". Una partita di ∀xA(x) o ∃xA(x) è una singola partita di A. La macchina vince ∀xA(x) (risp. ∃xA(x)) se tale partita è una vittoria di A(x) per tutti i valori possibili (risp. almeno un valore) di x.

Tutti gli operatori caratterizzati finora si comportano esattamente come le loro controparti classiche quando sono applicate a giochi elementari (senza mosse), e rendono validi gli stessi principi logici. Questo è il motivo per cui CoL usa gli stessi simboli della logica classica per quegli operatori. Quando tali operatori vengono applicati a giochi non elementari, tuttavia il loro comportamento non è più classico. Ad esempio, se p è un atomo elementare e P un atomo generale, p → (p ∧ p) è valido mentre P → (P ∧ P) non lo è. Tuttavia il principio del terzo escluso P ∨ ¬P rimane valido anche per atomi generali. Lo stesso principio, invece, non è valido con nessuno dei tre altri tipi (di scelta, sequenziale e commutante) di disgiunzione. La disgiunzione di scelta ⊔ ("chor") dei giochi A e B, scritta A ⊔ B, è un gioco in cui, per vincere, la macchina deve scegliere uno dei due disgiunti e poi vincere nel componente scelto. La disgiunzione sequenziale ("sor") A ᐁ B inizia giocando ad A e finisce anche con lo stesso gioco a meno che la macchina non abbia fatto una mossa di "inversione". In quel caso A viene abbandonato e il gioco ricomincia da capo e continua come B. Nella disgiunzione commutante (toggling disjunction, "tor") A ⩛ B, la macchina può passare tra A e B qualsiasi numero finito di volte. Ogni operatore di disgiunzione ha la sua congiunzione duale, ottenuta scambiando i ruoli dei due giocatori. I corrispondenti quantificatori possono essere definiti come congiunzioni o disgiunzioni infinite allo stesso modo dei quantificatori paralleli. Ogni tipo di disgiunzione permette anche di definire una corrispondente operazione di implicazione allo stesso modo che con l'implicazione parallela →. Ad esempio, l'implicazione di scelta ("chimplication") A⊐B è definita come ¬A ⊔ B.

Successivamente si può considerare il gruppo di operatori di ricorrenza. La ricorrenza parallela ("precurrence") di A può essere definita come la congiunzione parallela infinita A∧A∧A∧... I tipi sequenziale ("srecurrence") e commutante ("trecurrence") di ricorrenza possono essere definiti in modo simile. D'altra parte i corrispondenti operatori di coricorrenza possono essere invece definiti come disgiunzioni infinite. La ricorrenza ramificata ("brecurrence") ⫰, che è il tipo più forte di ricorrenza, non è definito a partire da corrispondente una congiunzione infinita. ⫰A è un gioco che inizia e procede come A. In qualsiasi momento, tuttavia, l'ambiente è autorizzato a fare una mossa "replicativa" che crea due copie della posizione attuale di A dividendo così il gioco in due "storie" parallele con un passato comune ma con sviluppi futuri eventualmente differenti. Allo stesso modo, l'ambiente può ulteriormente replicare qualsiasi posizione in ogni storia, creando così sempre più storie di A. Queste storie vengono giocate in parallelo, e la macchina deve vincere A in ognuna di esse per essere il vincitore di ⫰A. La coricorrenza ramificata ("cobrecurrence") ⫯ è definita simmetricamente scambiando "macchina" e "ambiente" fra loro.

Ogni tipo di ricorrenza induce inoltre una corrispondente versione debole dell'implicazione e della negazione. La prima è detta essere una implicazione ricorrente ("rimplication"), e la seconda una refutazione. L'implicazione ricorrente ramificata ("brimplication") A⟜B non è altro che ⫰A → B, e la confutazione ramificata di A è A⟜⊥, dove ⊥ è il gioco elementare (costante) che viene sempre perso. Per tutti gli altri tipi di rimplicazione e refutazione si procede analogamente.

• M. Bauer, A PSPACE-complete first order fragment of computability logic. ACM Transactions on Computational Logic 15 (2014), No 1, Article 1, 12 pages.
• M. Bauer, The computational complexity of propositional cirquent calculus. Logical Methods is Computer Science 11 (2015), Issue 1, Paper 12, pages 1-16.
• G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
• G. Japaridze, Propositional computability logic I. ACM Transactions on Computational Logic 7 (2006), pages 302-330.
• G. Japaridze, Propositional computability logic II. ACM Transactions on Computational Logic 7 (2006), pages 331-362.
• G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532. Prepublication
• G. Japaridze, Computability logic: a formal theory of interaction^{[collegamento interrotto]}. Interactive Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds. Springer Verlag, Berlin 2006, pages 183-223. Prepublication
• G. Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pages 100-135.
• G. Japaridze, From truth to computability II^{[collegamento interrotto]}. Theoretical Computer Science 379 (2007), pages 20–52.
• G. Japaridze, Intuitionistic computability logic. Acta Cybernetica 18 (2007), pages 77–113.
• G. Japaridze, The logic of interactive Turing reduction. Journal of Symbolic Logic 72 (2007), pages 243-276. Prepublication
• G. Japaridze, The intuitionistic fragment of computability logic at the propositional level^{[collegamento interrotto]}. Annals of Pure and Applied Logic 147 (2007), pages 187-227.
• G. Japaridze, Cirquent calculus deepened. Journal of Logic and Computation 18 (2008), No.6, pp. 983–1028.
• G. Japaridze, Sequential operators in computability logic^{[collegamento interrotto]}. Information and Computation 206 (2008), No.12, pp. 1443–1475. Prepublication
• G. Japaridze, Many concepts and two logics of algorithmic reduction^{[collegamento interrotto]}. Studia Logica 91 (2009), No.1, pp. 1–24. Prepublication
• G. Japaridze, In the beginning was game semantics. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249–350. Prepublication
• G. Japaridze, Towards applied theories based on computability logic. Journal of Symbolic Logic 75 (2010), pp. 565–601.
• G. Japaridze, Toggling operators in computability logic. Theoretical Computer Science 412 (2011), pp.  971-1004. Prepublication
• G. Japaridze, From formulas to cirquents in computability logic. Logical Methods in Computer Science 7 (2011), Issue 2, Paper 1, pp. 1-55.
• G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312-1354. Prepublication
• G. Japaridze, Separating the basic logics of the basic recurrences. Annals of Pure and Applied Logic 163 (2012), pp. 377-389. Prepublication
• G. Japaridze, A logical basis for constructive systems. Journal of Logic and Computation 22 (2012), pp. 605-642.
• G. Japaridze, A new face of the branching recurrence of computability logic. Applied Mathematics Letters 25 (2012),  1585-1589. Prepublication
• G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173-212. Prepublication
• G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part II. Archive for Mathematical Logic 52 (2013), pp. 213-259. Prepublication
• G. Japaridze, Introduction to clarithmetic III. Annals of Pure and Applied Logic 165 (2014),  241-252. Prepublication
• G. Japaridze, On the system CL12 of computability logic . Logical Methods is Computer Science 11 (2015), Issue 3, paper 1, pp. 1-71.
• G. Japaridze, Introduction to clarithmetic II. Information and Computation 247 (2016), pp. 290-312.
• G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1-59.
• G. Japaridze, Build your own clarithmetic II: Soundness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 12, pp. 1-62.
• K. Kwon, Expressing algorithms as concise as possible via computability logic. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, v. E97-A (2014), pp. 1385-1387.
• X. Li and J. Liu, Research on decidability of CoL2 in computability logic. Computer Science 42 (2015), No 7, pp. 44-46.
• I. Mezhirov and N. Vereshchagin, On abstract resource semantics and computability logic. Journal of Computer and System Sciences 76 (2010), pp. 356–372.
• M. Qu, J. Luan, D. Zhu and M. Du, On the toggling-branching recurrence of computability logic. Journal of Computer Science and Technology 28 (2013), pp. 278-284.
• N. Vereshchagin, Japaridze's computability logic and intuitionistic propositional calculus Archiviato il 3 marzo 2016 in Internet Archive.. Moscow State University, 2006.
• W. Xu and S. Liu, The countable versus uncountable branching recurrences in computability logic. Journal of Applied Logic 10 (2012), pp. 431-446.
• W. Xu and S. Liu, Soundness and completeness of the cirquent calculus system CL6 for computability logic. Logic Journal of the IGPL 20 (2012), pp. 317-330.
• W. Xu and S. Liu, The parallel versus branching recurrences in computability logic. Notre Dame Journal of Formal Logic 54 (2013), pp. 61-78.
• W. Xu, A propositional system induced by Japaridze’s approach to IF logic. Logic Journal of the IGPL 22 (2014), pp. 982-991
• W. Xu, A cirquent calculus system with clustering and ranking. Journal of Applied Logic 16 (2016), pp. 37-49.

• Computability Logic Homepage Comprehensive survey of the subject.
• Giorgi Japaridze
• Game Semantics or Linear Logic?
• Lecture Course on Computability Logic
• On abstract resource semantics and computabilty logic Video lecture by N.Vereshchagin.