Costruzione di realizzatori interattivi da prove in PRA+EM1 ed estrazione in Isabelle/HOL

The thesis proposes a realizability interpretation of a system for quantifier free arithmetic, which is equivalent to the fragment of classical arithmetic without nested quantifiers, called PRA+EM1. It based on Coquand's game theoretic semantics and learning in the limit of Gold: we look for an explicit description of the constructive meaning of proofs, possibly relating the obtained algorithms to the proof ideas they should come from. The basic intuition is that understanding proofs as learning strategies, by which a finite agent, called interactive realizer, learns to ensure the truth of the proof conclusion. Learning is an interactive process where the agent raises (general) hypothesis and tests them against (particular) facts, possibly realizing that some wrong guesses have been made. In those cases, she discards wrong guesses and changes her mind. We limit ourself to monotonic learning strategies, so that she can only abandon a branch in the search tree definitely (1-backtracking). 1-backtracking is enough to model learning strategies, which come from proofs using instances of excluded middle only over Σ^0_1 formulas (with parameters). Therefore, the realizer shall be able to find, going through a weakly increasing chain of knowledge states, a particular state where she can validate the formula, in a finite amount of time. Since the interpretation of formulas depends on the state, we have to extend the standard model using a strong monad: the state monad. The original contribute of the thesis consists of the construction of a interactive realizer from a proof of a formula in PRA+EM1, by induction on the syntactic rules of a deductive system built for PRA+EM1 (in which there are non logical axioms extracted from EM1). This construction needs another monad, namely realizer monad; such monad gives an operator to merge two different realizers, that have to validate the premises of a syntactic rule, so to obtain a new single interactive realizer that, in turn, has to validate its conclusion. In the second part of the thesis, there are practical applications of the theoretical notions exposed in the first part; in fact, a case of study is presented: the principle of minimum (PM). By using the logical framework Isabelle/HOL, the proof of PM is coded as a theory in Isabelle. Then, it is described how it is possible to extract from it a specific lambda term, called proof term, by means of the process of extraction embedded in Isabelle/HOL due at Berghofer's PhD thesis. In the last section, the thesis presents a guideline to obtain an interactive realizer from a proof term extracted from a classical proof coded in Isabelle/HOL, so that, in our case of study, it is possible obtain the realizer that shall be able to find a minimum point of the function.

La tesi propone una interpretazione costruttiva di un frammento dell'aritmetica classica senza quantificatori annidati, che chiamiamo PRA+EM1. Basandosi sui giochi semantici di Coquand e sul learning al limite di Gold, essa si concentra sull'estrazione di una strategia di apprendimento direttamente da una prova di una formula in PRA+EM1, che possa consentire ad un agente, detto realizzatore interattivo, di compiere una ricerca finalizzata alla scoperta di un testimone che renda vera la formula. La ricerca consiste nell'avanzamento di ipotesi circa un possibile candidato, che eventualmente possono essere smentite da evidenza contraria (controesempi), dando così la possibilità all'agente di ricredersi, dimenticando le proprie assunzioni, senza che esse possano di nuovo essere riconsiderate in futuro (1-backtracking). Dunque, il processo di learning è monotono e si dimostra che il 1-backtracking è sufficiente per poter estrapolare strategie ricorsive vincenti a partire da prove che sfruttano istanze di EM1, ovvero del terzo escluso ristretto a formule di Σ^0_1, consentendo così al realizzatore, attraversando una sequenza debolmente crescente di stati di conoscenza, di raggiungere, in un tempo finito, uno stato in cui sarà in grado di rendere vera la formula. Affinché l'interpretazione di una formula dipenda dallo stato di conoscenza in cui essa viene valutata dall'agente, viene ampliato il modello standard dell'aritmetica, mediante l'impiego di una strong monad: la state monad. Il contributo teorico consiste nella dimostrazione, per induzione sulle regole di un opportuno sistema deduttivo per PRA+EM1 (che include particolari assiomi non logici estrapolati da EM1), della costruzione di un realizzatore a partire dalla prova di una formula in PRA+EM1. Per far questo, abbiamo bisogno anche dell'introduzione di una opportuna monade, la monade dei realizzatori, che mette a disposizione anche una operazione, cosiddetta di merging, tra realizzatori di due premesse di una regola sintattica, al fine di ottenere quello che ne renda vera la conclusione. Nella sua seconda parte, la tesi si occupa di fornire delle applicazioni pratiche della proposta teorica di interpretazione costruttiva di PRA+EM1 fornita nella prima parte; dunque, viene presentato un caso di studio, il principio del minimo (PM), e sfruttando il theorem prover Isabelle/HOL, prima lo si dimostra e poi da tale derivazione logica si estrae un funzionale, detto proof term, seguendo una tecnica di estrazione che viene descritta ad hoc e che è oggetto della tesi di dottorato del Prof. Berghofer. Infine, si espone una linea guida teorica per poter ottenere, in modo automatico, partendo da un proof term proprio un realizzatore interattivo, che, nel caso del PM, operando la sua strategia di ricerca, riesce a trovare un punto di minimo per la funzione.