-
Higher-order Games with Dependent Types
Authors:
Martín Escardó,
Paulo Oliva
Abstract:
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point.…
▽ More
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point. In particular, games are modelled by a W-type, which is essentially the same type used by Aczel to model constructive Zermelo-Frankel set theory (CZF). We have also implemented all our definitions, constructions, results and proofs in the dependently-typed programming language Agda, which, in particular, allows us to run concrete examples of computations of optimal strategies, that is, strategies in subgame perfect equilibrium.
△ Less
Submitted 7 July, 2023; v1 submitted 15 December, 2022;
originally announced December 2022.
-
Quantification of pulmonary involvement in COVID-19 pneumonia by means of a cascade oftwo U-nets: training and assessment on multipledatasets using different annotation criteria
Authors:
Francesca Lizzi,
Abramo Agosti,
Francesca Brero,
Raffaella Fiamma Cabini,
Maria Evelina Fantacci,
Silvia Figini,
Alessandro Lascialfari,
Francesco Laruina,
Piernicola Oliva,
Stefano Piffer,
Ian Postuma,
Lisa Rinaldi,
Cinzia Talamonti,
Alessandra Retico
Abstract:
The automatic assignment of a severity score to the CT scans of patients affected by COVID-19 pneumonia could reduce the workload in radiology departments. This study aims at exploiting Artificial intelligence (AI) for the identification, segmentation and quantification of COVID-19 pulmonary lesions. We investigated the effects of using multiple datasets, heterogeneously populated and annotated ac…
▽ More
The automatic assignment of a severity score to the CT scans of patients affected by COVID-19 pneumonia could reduce the workload in radiology departments. This study aims at exploiting Artificial intelligence (AI) for the identification, segmentation and quantification of COVID-19 pulmonary lesions. We investigated the effects of using multiple datasets, heterogeneously populated and annotated according to different criteria. We developed an automated analysis pipeline, the LungQuant system, based on a cascade of two U-nets. The first one (U-net_1) is devoted to the identification of the lung parenchyma, the second one (U-net_2) acts on a bounding box enclosing the segmented lungs to identify the areas affected by COVID-19 lesions. Different public datasets were used to train the U-nets and to evaluate their segmentation performances, which have been quantified in terms of the Dice index. The accuracy in predicting the CT-Severity Score (CT-SS) of the LungQuant system has been also evaluated. Both Dice and accuracy showed a dependency on the quality of annotations of the available data samples. On an independent and publicly available benchmark dataset, the Dice values measured between the masks predicted by LungQuant system and the reference ones were 0.95$\pm$0.01 and 0.66$\pm$0.13 for the segmentation of lungs and COVID-19 lesions, respectively. The accuracy of 90% in the identification of the CT-SS on this benchmark dataset was achieved. We analysed the impact of using data samples with different annotation criteria in training an AI-based quantification system for pulmonary involvement in COVID-19 pneumonia. In terms of the Dice index, the U-net segmentation quality strongly depends on the quality of the lesion annotations. Nevertheless, the CT-SS can be accurately predicted on independent validation sets, demonstrating the satisfactory generalization ability of the LungQuant.
△ Less
Submitted 6 May, 2021;
originally announced May 2021.
-
On the Herbrand Functional Interpretation
Authors:
Paulo Oliva,
Chuangjie Xu
Abstract:
We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigatio…
▽ More
We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigation we also strengthen the monotonicity property of the original presentation, and prove a monotonicity property for our alternative definition.
△ Less
Submitted 3 December, 2019;
originally announced December 2019.
-
Negative Translations for Affine and Lukasiewicz Logic
Authors:
Rob Arthan,
Paulo Oliva
Abstract:
We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend af…
▽ More
We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and vice versa. By contrast, in the setting of Lukasiewicz logic, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, Gödel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Lukasiewicz logic but are all equivalent.
△ Less
Submitted 29 November, 2019;
originally announced December 2019.
-
Studying Algebraic Structures using Prover9 and Mace4
Authors:
Rob Arthan,
Paulo Oliva
Abstract:
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a class of algebraic structures. We will see that these tools, when combined with human insight and traditional algebraic methods, help us to explore the problem space quickly and effectively. The…
▽ More
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a class of algebraic structures. We will see that these tools, when combined with human insight and traditional algebraic methods, help us to explore the problem space quickly and effectively. The counter-example generator rapidly rules out many false conjectures, while the theorem prover is often much more efficient than a human being at verifying algebraic identities. The specific tools in our case study are Prover9 and Mace4; the algebraic structures are generalisations of Heyting algebras known as hoops. We will see how this approach helped us to discover new theorems and to find new or improved proofs of known results. We also make some suggestions for how one might deploy these tools to supplement a more conventional approach to teaching algebra.
△ Less
Submitted 14 August, 2019;
originally announced August 2019.
-
A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic
Authors:
Rob Arthan,
Paulo Oliva
Abstract:
In this paper we introduce a term calculus ${\cal B}$ which adds to the affine $λ$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between ${\cal B}$ and the sub-structural logical system which we call "minimal Łukasiewicz logic", also known in the literature as the logic of hoops (a generalisation of MV-algebras). This l…
▽ More
In this paper we introduce a term calculus ${\cal B}$ which adds to the affine $λ$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between ${\cal B}$ and the sub-structural logical system which we call "minimal Łukasiewicz logic", also known in the literature as the logic of hoops (a generalisation of MV-algebras). This logic lies strictly in between affine minimal logic and standard minimal logic. We prove that ${\cal B}$ is strongly normalising and has the Church-Rosser property. We also give examples of terms in ${\cal B}$ corresponding to some important derivations from our work and the literature. Finally, we discuss the relation between normalisation in ${\cal B}$ and cut-elimination for a Gentzen-style formulation of minimal Łukasiewicz logic.
△ Less
Submitted 12 September, 2018;
originally announced September 2018.
-
On Rational Choice and the Representation of Decision Problems
Authors:
Paulo Oliva,
Philipp Zahn
Abstract:
In economic theory, an agent chooses from available alternatives -- modeled as a set. In decisions in the field or in the lab, however, agents do not have access to the set of alternatives at once. Instead, alternatives are represented by the outside world in a structured way. Online search results are lists of items, wine menus are often lists of lists (grouped by type or country), and online sho…
▽ More
In economic theory, an agent chooses from available alternatives -- modeled as a set. In decisions in the field or in the lab, however, agents do not have access to the set of alternatives at once. Instead, alternatives are represented by the outside world in a structured way. Online search results are lists of items, wine menus are often lists of lists (grouped by type or country), and online shopping often involves filtering items which can be viewed as navigating a tree. Representations constrain how an agent can choose. At the same time, an agent can also leverage representations when choosing, simplifying his/her choice process. For instance, in the case of a list he or she can use the order in which alternatives are represented to make his/her choice.
In this paper, we model representations and decision procedures operating on them. We show that choice procedures are related to classical choice functions by a canonical mapping. Using this mapping, we can ask whether properties of choice functions can be lifted onto the choice procedures which induce them. We focus on the obvious benchmark: rational choice. We fully characterize choice procedures which can be rationalized by a strict preference relation for general representations including lists, list of lists, trees and others. Our framework can thereby be used as the basis for new tests of rational behavior.
Classical choice theory operates on very limited information, typically budgets or menus and final choices. This is in stark contrast to the vast amount of data that specifically web companies collect about their users' choice process. Our framework offers a way to integrate such data into economic choice models.
△ Less
Submitted 8 November, 2021; v1 submitted 10 January, 2018;
originally announced January 2018.
-
Higher-Order Decision Theory
Authors:
Jules Hedges,
Paulo Oliva,
Evguenia Sprits,
Viktor Winschel,
Philipp Zahn
Abstract:
Classical decision theory models behaviour in terms of utility maximisation where utilities represent rational preference relations over outcomes. However, empirical evidence and theoretical considerations suggest that we need to go beyond this framework. We propose to represent goals by higher-order functions or operators that take other functions as arguments where the max and argmax operators a…
▽ More
Classical decision theory models behaviour in terms of utility maximisation where utilities represent rational preference relations over outcomes. However, empirical evidence and theoretical considerations suggest that we need to go beyond this framework. We propose to represent goals by higher-order functions or operators that take other functions as arguments where the max and argmax operators are special cases. Our higher-order functions take a context function as their argument where a context represents a process from actions to outcomes. By that we can define goals being dependent on the actions and the process in addition to outcomes only. This formulation generalises outcome based preferences to context-dependent goals. We show how to uniformly represent within our higher-order framework classical utility maximisation but also various other extensions that have been debated in economics.
△ Less
Submitted 3 June, 2015; v1 submitted 2 June, 2015;
originally announced June 2015.
-
Higher-Order Game Theory
Authors:
Jules Hedges,
Paulo Oliva,
Evguenia Sprits,
Viktor Winschel,
Philipp Zahn
Abstract:
In applied game theory the motivation of players is a key element. It is encoded in the payoffs of the game form and often based on utility functions. But there are cases were formal descriptions in the form of a utility function do not exist. In this paper we introduce a representation of games where players' goals are modeled based on so-called higher-order functions. Our representation provides…
▽ More
In applied game theory the motivation of players is a key element. It is encoded in the payoffs of the game form and often based on utility functions. But there are cases were formal descriptions in the form of a utility function do not exist. In this paper we introduce a representation of games where players' goals are modeled based on so-called higher-order functions. Our representation provides a general and powerful way to mathematically summarize players' intentions. In our framework utility functions as well as preference relations are special cases to describe players' goals. We show that in higher-order functions formal descriptions of players may still exist where utility functions do not using a classical example, a variant of Keynes' beauty contest. We also show that equilibrium conditions based on Nash can be easily adapted to our framework. Lastly, this framework serves as a stepping stone to powerful tools from computer science that can be usefully applied to economic game theory in the future such as computational and computability aspects.
△ Less
Submitted 3 June, 2015; v1 submitted 2 June, 2015;
originally announced June 2015.
-
Spector bar recursion over finite partial functions
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recu…
▽ More
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recursive updates, terminating the computation whenever $\varphi(\hat{u})\in\mbox{dom}(u)$. We begin by exploring theoretical aspects of this new form of recursion, then in the main part of the paper we show that demand-driven bar recursion can be directly used to give an alternative functional interpretation of classical countable choice. We provide a short case study as an illustration, in which we extract a new bar recursive program from the proof that there is no injection from $\mathbb{N}\to\mathbb{N}$ to $\mathbb{N}$, and compare this to the program that would be obtained using Spector's original variant. We conclude by formally establishing that our new bar recursor is primitive recursively equivalent to the original Spector bar recursion, and thus defines the same class of functionals when added to Gödel's system $\sf T$.
△ Less
Submitted 17 August, 2015; v1 submitted 23 October, 2014;
originally announced October 2014.
-
Unifying Functional Interpretations: Past and Future
Authors:
Paulo Oliva
Abstract:
This article surveys work done in the last six years on the unification of various functional interpretations including Gödel's dialectica interpretation, its Diller-Nahm variant, Kreisel modified realizability, Stein's family of functional interpretations, functional interpretations "with truth", and bounded functional interpretations. Our goal in the present paper is twofold: (1) to look back an…
▽ More
This article surveys work done in the last six years on the unification of various functional interpretations including Gödel's dialectica interpretation, its Diller-Nahm variant, Kreisel modified realizability, Stein's family of functional interpretations, functional interpretations "with truth", and bounded functional interpretations. Our goal in the present paper is twofold: (1) to look back and single out the main lessons learnt so far, and (2) to look forward and list several open questions and possible directions for further research.
△ Less
Submitted 16 October, 2014;
originally announced October 2014.
-
The Herbrand Functional Interpretation of the Double Negation Shift
Authors:
Martin Escardo,
Paulo Oliva
Abstract:
This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection…
▽ More
This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector's bar recursion. We then prove several properties of this product in the special case when $T$ is the finite power set monad ${\mathcal P}(\cdot)$. These are used to show that when $T X = {\mathcal P}(X)$ the explicitly controlled product of $T$-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.
△ Less
Submitted 19 October, 2015; v1 submitted 16 October, 2014;
originally announced October 2014.
-
A Higher-order Framework for Decision Problems and Games
Authors:
Jules Hedges,
Paulo Oliva,
Evguenia Winschel,
Viktor Winschel,
Philipp Zahn
Abstract:
We introduce a new unified framework for modelling both decision problems and finite games based on quantifiers and selection functions. We show that the canonical utility maximisation is one special case of a quantifier and that our more abstract framework provides several additional degrees of freedom in modelling. In particular, incomplete preferences, non-maximising heuristics, and context-dep…
▽ More
We introduce a new unified framework for modelling both decision problems and finite games based on quantifiers and selection functions. We show that the canonical utility maximisation is one special case of a quantifier and that our more abstract framework provides several additional degrees of freedom in modelling. In particular, incomplete preferences, non-maximising heuristics, and context-dependent motives can be taken into account when describing an agent's goal. We introduce a suitable generalisation of Nash equilibrium for games in terms of quantifiers and selection functions. Moreover, we introduce a refinement of Nash that captures context-dependency of goals. Modelling in our framework is compositional as the parts of the game are modular and can be easily exchanged. We provide an extended example where we illustrate concepts and highlight the benefits of our alternative modelling approach.
△ Less
Submitted 25 September, 2014;
originally announced September 2014.
-
Proceedings Fifth International Workshop on Classical Logic and Computation
Authors:
Paulo Oliva
Abstract:
Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the exploration of the computational content of mathematical and logical principles, aiming to bring together researchers from both fields and exchange ideas. In this fifth…
▽ More
Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the exploration of the computational content of mathematical and logical principles, aiming to bring together researchers from both fields and exchange ideas. In this fifth edition we received 18 submissions of both short and full papers. Fourteen (14) of these were selected to present at the meeting in Vienna, and six (6) full papers were accepted to appear at this ETPCS special volume. Topics covered by this years submissions included: translations of classical to intuitionistic proofs, witness extraction from classical proofs, confluence properties for classical systems, linear logic, constructive semantics for classical logic (game semantics, realizability), and the study of calculi based on classical logic (lambda-mu-calculus, continuation calculus).
△ Less
Submitted 9 September, 2014;
originally announced September 2014.
-
Bar Recursion and Products of Selection Functions
Authors:
Martin Escardo,
Paulo Oliva
Abstract:
We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown t…
▽ More
We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of "skewed" selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to be T-equivalent to the iteration of the simple products.
△ Less
Submitted 14 August, 2014; v1 submitted 25 July, 2014;
originally announced July 2014.
-
Proving termination with transition invariants of height omega
Authors:
Stefano Berardi,
Paulo Oliva,
Silvia Steila
Abstract:
The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a…
▽ More
The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a "disjunctively well-founded transition invariant". From this result the same authors and Byron Cook designed an algorithm checking a sufficient condition for termination for a while-if program. The algorithm looks for a disjunctively well-founded transition invariant, made of well-founded relations of height omega, and if it finds it, it deduces the termination for the while-if program using the Termination Theorem.
This raises an interesting question: What is the status of reduction relations having a disjunctively well-founded transition invariant where each relation has height omega? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating. The goal of this work is to prove that they are exactly the set of reduction relations having height omega^n for some n < omega. Besides, if all the relations in the transition invariant are primitive recursive and the reduction relation is the graph of the restriction to some primitive recursive set of a primitive recursive map, then a final state is computable by some primitive recursive map in the initial state.
As a corollary we derive that the set of functions, having at least one implementation in Podelski Rybalchenko while-if language with a well-founded disjunctively transition invariant where each relation has height omega, is exactly the set of primitive recursive functions.
△ Less
Submitted 17 July, 2014;
originally announced July 2014.
-
On Pocrims and Hoops
Authors:
Rob Arthan,
Paulo Oliva
Abstract:
Pocrims and suitable specialisations thereof are structures that provide the natural algebraic semantics for a minimal affine logic and its extensions. Hoops comprise a special class of pocrims that provide algebraic semantics for what we view as an intuitionistic analogue of the classical multi-valued Łukasiewicz logic. We present some contributions to the theory of these algebraic structures. We…
▽ More
Pocrims and suitable specialisations thereof are structures that provide the natural algebraic semantics for a minimal affine logic and its extensions. Hoops comprise a special class of pocrims that provide algebraic semantics for what we view as an intuitionistic analogue of the classical multi-valued Łukasiewicz logic. We present some contributions to the theory of these algebraic structures. We give a new proof that the class of hoops is a variety. We use a new indirect method to establish several important identities in the theory of hoops: in particular, we prove that the double negation mapping in a hoop is a homormorphism. This leads to an investigation of algebraic analogues of the various double negation translations that are well-known from proof theory. We give an algebraic framework for studying the semantics of double negation translations and use it to prove new results about the applicability of the double negation translations due to Gentzen and Glivenko.
△ Less
Submitted 16 October, 2014; v1 submitted 3 April, 2014;
originally announced April 2014.
-
On Affine Logic and Łukasiewicz Logic
Authors:
Rob Arthan,
Paulo Oliva
Abstract:
The multi-valued logic of Łukasiewicz is a substructural logic that has been widely studied and has many interesting properties. It is classical, in the sense that it admits the axiom schema of double negation, [DNE]. However, our understanding of Łukasiewicz logic can be improved by separating its classical and intuitionistic aspects. The intuitionistic aspect of Łukasiewicz logic is captured in…
▽ More
The multi-valued logic of Łukasiewicz is a substructural logic that has been widely studied and has many interesting properties. It is classical, in the sense that it admits the axiom schema of double negation, [DNE]. However, our understanding of Łukasiewicz logic can be improved by separating its classical and intuitionistic aspects. The intuitionistic aspect of Łukasiewicz logic is captured in an axiom schema, [CWC], which asserts the commutativity of a weak form of conjunction. This is equivalent to a very restricted form of contraction. We show how Łukasiewicz Logic can be viewed both as an extension of classical affine logic with [CWC], or as an extension of what we call \emph{intuitionistic} Łukasiewicz logic with [DNE], intuitionistic Łukasiewicz logic being the extension of intuitionistic affine logic by the schema [CWC]. At first glance, intuitionistic affine logic seems very weak, but, in fact, [CWC] is surprisingly powerful, implying results such as intuitionistic analogues of De Morgan's laws. However the proofs can be very intricate. We present these results using derived connectives to clarify and motivate the proofs and give several applications. We give an analysis of the applicability to these logics of the well-known methods that use negation to translate classical logic into intuitionistic logic. The usual proofs of correctness for these translations make much use of contraction. Nonetheless, we show that all the usual negative translations are already correct for intuitionistic Łukasiewicz logic, where only the limited amount of contraction given by [CWC] is allowed. This is in contrast with affine logic for which we show, by appeal to results on semantics proved in a companion paper, that both the Gentzen and the Glivenko translations fail.
△ Less
Submitted 14 August, 2014; v1 submitted 2 April, 2014;
originally announced April 2014.
-
Project G.N.O.S.I.S.: Geographical Network Of Synoptic Information System
Authors:
Pietro Oliva
Abstract:
Everybody knows how much synoptic maps are useful today. An excellent example above all is Google Earth: its simplicity and friendly interface allows every user to have the Earth maps ready in just one simple layout; nevertheless a crucial dimension is missing in Google Earth: the time. This doesn't mean we simply aim to add history to Google Earth (though it could be already a nice goal): the mai…
▽ More
Everybody knows how much synoptic maps are useful today. An excellent example above all is Google Earth: its simplicity and friendly interface allows every user to have the Earth maps ready in just one simple layout; nevertheless a crucial dimension is missing in Google Earth: the time. This doesn't mean we simply aim to add history to Google Earth (though it could be already a nice goal): the main idea behind GNOSIS project is to produce applications to "dress up" the Globe with a set of skin-maps representing the most various different kind of histories like the evolution of geology, genetics, agriculture, ethnology, linguistics, musicology, metallurgy and so forth, in time. It may be interesting in the near future to have such a possibility to watch on the map the positions and movements of the armies during the battles of Waterloo or Thermopylae, the spreading of the cultivation of corn in time, the rise and fall of Roman Empire or the diffusion of Smallpox together with the spread of a religion, a specific dialect, the early pottery techniques or the natural resources available to pre-Columbian civilizations on a Google-Earth-map-like, that is to say to have at one's hand the ultimate didactic-enciclopedic tool. To do so we foresee the use of a general-purpose intermediate/high level programming language, possibly object-oriented such C++ or Java.
△ Less
Submitted 3 November, 2012;
originally announced November 2012.
-
A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
△ Less
Submitted 1 June, 2012; v1 submitted 25 April, 2012;
originally announced April 2012.
-
A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the prod…
▽ More
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the product gives these theorems a natural computational interpretation that can be clearly understood in game theoretic terms.
△ Less
Submitted 23 April, 2012;
originally announced April 2012.
-
(Dual) Hoops Have Unique Halving
Authors:
Rob Arthan,
Paulo Oliva
Abstract:
Continuous logic extends the multi-valued Lukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The semantics of these logics can be given using specialisations of algebraic structures known as hoops. As part of an investigation into the metatheory of propositional continuous logic, we were ind…
▽ More
Continuous logic extends the multi-valued Lukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The semantics of these logics can be given using specialisations of algebraic structures known as hoops. As part of an investigation into the metatheory of propositional continuous logic, we were indebted to Prover9 for finding a proof of an important algebraic law.
△ Less
Submitted 14 October, 2013; v1 submitted 2 March, 2012;
originally announced March 2012.
-
On Various Negative Translations
Authors:
Gilda Ferreira,
Paulo Oliva
Abstract:
Several proof translations of classical mathematics into intuitionistic mathematics have been proposed in the literature over the past century. These are normally referred to as negative translations or double-negation translations. Among those, the most commonly cited are translations due to Kolmogorov, Godel, Gentzen, Kuroda and Krivine (in chronological order). In this paper we propose a framew…
▽ More
Several proof translations of classical mathematics into intuitionistic mathematics have been proposed in the literature over the past century. These are normally referred to as negative translations or double-negation translations. Among those, the most commonly cited are translations due to Kolmogorov, Godel, Gentzen, Kuroda and Krivine (in chronological order). In this paper we propose a framework for explaining how these different translations are related to each other. More precisely, we define a notion of a (modular) simplification starting from Kolmogorov translation, which leads to a partial order between different negative translations. In this derived ordering, Kuroda and Krivine are minimal elements. Two new minimal translations are introduced, with Godel and Gentzen translations sitting in between Kolmogorov and one of these new translations.
△ Less
Submitted 27 January, 2011;
originally announced January 2011.
-
Functional Interpretations of Intuitionistic Linear Logic
Authors:
Gilda Ferreira,
Paulo Oliva
Abstract:
We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic logic IL via embeddings of IL into ILL. The main difference from previous work of the second author is that in intuitionistic linear logic (as opposed to classical linear logic) the interpretations of !A are simpler and s…
▽ More
We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic logic IL via embeddings of IL into ILL. The main difference from previous work of the second author is that in intuitionistic linear logic (as opposed to classical linear logic) the interpretations of !A are simpler and simultaneous quantifiers are no longer needed for the characterisation of the interpretations. We then compare our approach in developing these three proof interpretations with the one of de Paiva around the Dialectica category model of linear logic.
△ Less
Submitted 24 March, 2011; v1 submitted 6 December, 2010;
originally announced December 2010.
-
A General Framework for Sound and Complete Floyd-Hoare Logics
Authors:
Rob Arthan,
Ursula Martin,
Erik A. Mathiesen,
Paulo Oliva
Abstract:
This paper presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of pre-orders and monotone relations. We give several examples of how our theory generalises usual Hoare logics (partial correctness of whil…
▽ More
This paper presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of pre-orders and monotone relations. We give several examples of how our theory generalises usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs), and provide some case studies on how it can be used to develop new Hoare logics (run-time analysis of while programs and stream circuits).
△ Less
Submitted 7 July, 2008;
originally announced July 2008.
