arXiv subjects

José Espírito Santo

Publications and source records attributed to José Espírito Santo.

10 recordsLinked to original sources

arXiv2025

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. Inhabitation is taken in a generalized sense, because we also consider when a sequent has a solution, that is a (possibly infinite) run of bottom-up proof search which never fails to apply another inference rule. We provide a very general scheme whose instances are decision problems concerning solutions in LJP having algorithms through the inductive syntax. Polarized logic and LJP can be used as a platform from which proof search for other logics is understood. We illustrate this for the proof systems LJT and LJQ for intuitionistic logic, both equipped with all the connectives. For that we work out respectively a negative and a positive interpretation into LJP, which map formulas of the source logic into formulas in LJP of the said polarity; and this even at the level of the coinductive versions of the three involved proof systems. The interpretations are proved to be, not only faithful, but actually full embeddings, establishing a bijection between the solutions (resp. proofs) of a sequent and the solutions (resp. proofs) of its polarized interpretation. This allows the inheritance to the source systems of the decidability and other results previously obtained for LJP, thereby vastly generalizing the previous results of CoIPS, which were confined to LJT and implicational intuitionistic logic.

cs.LO↗

arXiv2024

A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications

We introduce a call-by-name lambda-calculus $λJn$ with generalized applications which is equipped with distant reduction. This allows to unblock $β$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $ΛJ$-calculus with generalized applications of Joachimski and Matthes. We show strong normalization of simply-typed terms, and we then fully characterize strong normalization by means of a quantitative (i.e. non-idempotent intersection) typing system. This characterization uses a non-trivial inductive definition of strong normalization --related to others in the literature--, which is based on a weak-head normalizing strategy. We also show that our calculus $λJn$ relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus $λJn$ and the original $ΛJ$-calculus determine equivalent notions of strong normalization. As a consequence, $λJ$ inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative typing system designed for $λJn$, despite the fact that quantitative subject reduction fails for permutative conversions.

cs.LO↗

arXiv2024

How to avoid the commuting conversions of IPC

Since the observation in 2006 that it is possible to embed IPC into the atomic polymorphic lambda-calculus (a predicative fragment of system F with universal instantiations restricted to atomic formulas) different such embeddings appeared in the literature. All of them comprise the Russell-Prawitz translation of formulas, but have different strategies for the translation of proofs. Although these embeddings preserve proof identity, all fail in delivering preservation of reduction steps. In fact, they translate the commuting conversions of IPC to beta-equality, or to other kinds of reduction or equality generated by new principles added to system F. The cause for this is the generation of redexes by the translation itself. In this paper, we present an embedding of IPC into atomic system F, still based on the same translation of formulas, but which maps commuting conversions to syntactic identity, while simulating the other kinds of reduction steps present in IPC betaη-reduction. In this sense the translation achieves a truly commuting conversion-free image of IPC in atomic system F.

cs.LO↗

arXiv2023

The Logical Essence of Compiling With Continuations

The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi's computational lambda-calculus (lbc), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the "essence" of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of lbc, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations.

cs.LO↗

arXiv2021

A Coinductive Approach to Proof Search through Typed Lambda-Calculi

In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard paradigm of representation, from proofs to solutions: to represent solutions by possibly infinite terms of a dedicated lambda-calculus. This new, comprehensive approach to proof search is exemplified with the sequent calculus LJT for intuitionistic implication logic. A finitary representation is proposed, comprising lambda-terms extended with a formal greatest fixed point, and a type system that can be seen as a logic of coinductive proofs. In the finitary system, fixed-point variables enjoy a relaxed form of binding that allows the detection of cycles through the type system. Formal sums are used to express alternatives in the search process. Moreover, formal sums are used in the coinductive syntax to define "decontraction" (contraction bottom-up) - an operation whose theory we initiate in this paper. As a semantics, we assign a coinductive lambda-term to each finitary term. The main result is the existence of an equivalent finitary representation for any full solution space expressed coinductively. This result is the main ingredient in the proof that our logic of coinductive proofs is sound and complete with respect to the coinductive semantics. These results are the foundation for an original approach to proof search, where the search builds the finitary representation of the full solution space, and the a posteriori analysis typically consisting in applying a syntax-directed procedure or function. The paper illustrates this for proof search and inhabitation problems in the simply-typed lambda-calculus, reviewing results detailed elsewhere, and including new results that obtain extensive generalizations of the so-called monatomic theorem.

cs.LO↗

arXiv2020

The Russell-Prawitz embedding and the atomization of universal instantiation

Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system F_at, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain "dinaturality" conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system F_at; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into F_at does not.

math.LO↗

arXiv2017

Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search

A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and the end products are simple, recursive decision procedures and counting functions.

cs.LO↗

arXiv2016

A note on strong normalization in classical natural deduction

In the context of natural deduction for propositional classical logic, with classicality given by the inference rule reductio ad absurdum, we investigate the De Morgan translation of disjunction in terms of negation and conjunction. Once the translation is extended to proofs, it obtains a reduction of provability to provability in the disjunction-free subsystem. It is natural to ask whether a reduction is also obtained for, say, strong normalization; that is, whether strong normalization for the disjunction-free system implies the same property for the full system, and whether such lifting of the property can be done along the De Morgan translation. Although natural, these questions are neglected by the literature. We spell out the map of reduction steps induced by the De Morgan translation of proofs. But we need to "optimize" such a map in order to show that a reduction sequence in the full system from a proof determines, in a length-preserving way, a reduction sequence in the disjunction-free system from the De Morgan translation of the proof. In this sense, the above questions have a positive answer.

cs.LO↗

arXiv2014

Confluence for classical logic through the distinction between values and computations

We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's lambda-bar-mu-mu-tilde-calculus without losing confluence, and is based on a distinction of "modes" in the proof expressions and "mode" annotations in types. Modes resemble colors and polarities, but are quite different: we give meaning to them in terms of a monadic meta-language where the distinction between values and computations is fully explored. This meta-language is a refinement of the classical monadic language previously introduced by the authors, and is also developed in the paper.

cs.LO↗

arXiv2013

A Coinductive Approach to Proof Search

We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the "solution spaces" (called Böhm forests), which are a representation of all (not necessarily well-founded but still locally well-formed) proofs of a given formula (more generally: of a given sequent). As main result we obtain, for each given formula, the reduction of a coinductive definition of the solution space to a effective coinductive description in a finitary term calculus with a formal greatest fixed-point operator. This reduction works in a quite direct manner for the case of Horn formulas. For the general case, the naive extension would not even be true. We need to study "co-contraction" of contexts (contraction bottom-up) for dealing with the varying contexts needed beyond the Horn fragment, and we point out the appropriate finitary calculus, where fixed-point variables are typed with sequents. Co-contraction enters the interpretation of the formal greatest fixed points - curiously in the semantic interpretation of fixed-point variables and not of the fixed-point operator.

cs.LO↗