Wikipedia

Logica della computabilità

Versione del 22 mag 2017 alle 16:43 di Nemoeximius (discussione | contributi) (Aggiunta Immagine in sezione Linguaggio: tabella degli operatori della CoL)

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 B1, ...,Bn. Inoltre, la CoL fornisce un metodo uniforme per realizzare effettivamente una soluzione (algoritmo) di tale problema A da qualsiasi soluzione nota di B1, ..., Bn.

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 prioprie 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 Circuenti[6][7].

Linguaggio

 
Operatori della Logica della computabilità

Il linguaggio completo della CoL è un'estensione del linguaggio della Logica classica 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 prioprio del linguaggio.

Letteratura

Collegamenti Esterni

Note

  1. ^ G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.
  2. ^ 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
  3. ^ G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187-227.
  4. ^ G. Japaridze, Introduction to clarithmetic I. Information and Computation 209 (2011), pp. 1312-1354. Prepublication
  5. ^ G. Japaridze, Build your own clarithmetic I: Setup and completeness. Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pp. 1-59.
  6. ^ G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532. Prepublication
  7. ^ G. Japaridze, The taming of recurrences in computability logic through cirquent calculus, Part I. Archive for Mathematical Logic 52 (2013), pp. 173-212. Prepublication
Estratto da "https://it.wikipedia.org/w/index.php?title=Logica_della_computabilità&oldid=87970048"