arXiv subjects

Paulo Oliva

Publications and source records attributed to Paulo Oliva.

32 records · Page 2Linked to original sources

arXiv2014

On Pocrims and Hoops

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.

math.LO↗

arXiv2014

Unifying Functional Interpretations: Past and Future

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.

math.LO↗

arXiv2014

A Higher-order Framework for Decision Problems and Games

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.

cs.LO↗

arXiv2014

Proceedings Fifth International Workshop on Classical Logic and Computation

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).

cs.LO↗

arXiv2014

On Affine Logic and Łukasiewicz Logic

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.

cs.LO↗

arXiv2014

Bar Recursion and Products of Selection Functions

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.

cs.LO↗

arXiv2014

Proving termination with transition invariants of height omega

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.

cs.LO↗

arXiv2013

(Dual) Hoops Have Unique Halving

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.

cs.AI↗

arXiv2012

Hoops, Coops and the Algebraic Semantics of Continuous Logic

Büchi and Owen studied algebraic structures called hoops. Hoops provide a natural algebraic semantics for a class of substructural logics that we think of as intuitionistic analogues of the widely studied Łukasiewicz logics. Ben Yaacov extended Łukasiewicz logic to get what is called continuous logic by adding a halving operator. In this paper, we define the notion of continuous hoop, or coop for short, and show that coops provide a natural algebraic semantics for continuous logic. We characterise the simple and subdirectly irreducible coops and investigate the decision problem for various theories of coops. In passing, we give a new proof that hoops form a variety by giving an algorithm that converts a proof in intuitionistic Łukaseiwicz logic into a chain of equations.

math.LO↗

arXiv2012

A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions

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.

math.LO↗

arXiv2012

A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis

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.

math.LO↗

arXiv2011

Functional Interpretations of Intuitionistic Linear Logic

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.

cs.LO↗

arXiv2011

On Various Negative Translations

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.

cs.LO↗

arXiv2008

A General Framework for Sound and Complete Floyd-Hoare Logics

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).

cs.LO↗