Stefano Berardi

TCS Journal 2025 Journal Article

Termination of rewriting on reversible Boolean circuits as a free 3-category problem

• Adriano Barile
• Stefano Berardi
• Luca Roversi

Reversible Boolean Circuits are an interesting computational model under many aspects and in different fields, ranging from Reversible Computing to Quantum Computing. Our contribution is to describe a specific class of Reversible Boolean Circuits - which is as expressive as classical circuits - as a bi-dimensional diagrammatic programming language. We uniformly represent the Reversible Boolean Circuits we focus on as a free 3-category Toff. This formalism allows us to incorporate the representation of circuits and of rewriting rules on them, and to prove termination of rewriting. Termination follows from defining a non-identities-preserving functor from our free 3-category Toff into a suitable 3-category Move that traces the “moves” applied to wires inside circuits.

CSL Conference 2024 Conference Paper

A General Constructive Form of Higman's Lemma

• Stefano Berardi
• Gabriele Buriola
• Peter Schuster 0001

In logic and computer science one often needs to constructivize a theorem ∀ f ∃ g. P(f, g), stating that for every infinite sequence f there is an infinite sequence g such that P(f, g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of ∀ f ∃ g. P(f, g): for every f there is a "long enough" finite prefix g₀ of g such that P(f, g₀), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version. Our approach with bars generalises the approaches to Higman’s lemma undertaken by Coquand-Fridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman’s lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman’s lemma, our constructive proofs are closer to the original classical proofs.

CSL Conference 2015 Conference Paper

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness

• Stefano Berardi

Assume that we may prove in Classical Functional Analysis that a primitive recursive relation R is well-founded, using the inductive definition of well-founded. In this paper we prove that such a proof of well-foundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive well-foundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of well-foundation we may always find an intuitionistic proof if we may find a proof at all. The core of intuitionism are the methods for computing out data with given properties from input data with given properties: these are the results we are looking for when we do constructive mathematics. Proving that a primitive recursive relation R is inductively well-founded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively well-founded, then we may write programs by induction over R. This is the way inductive relation are currently used in intuitionism and in proof assistants based on intuitionism, like Coq. In the paper we introduce the comprehension axiom for Functional Analysis in the form of introduction and elimination rules for predicates of types Prop, Nat->Prop, .. ., in order to use Girard's method of candidates for impredicative arithmetic.

CSL Conference 2013 Conference Paper

Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1

• Federico Aschieri
• Stefano Berardi
• Giovanni Birolo

We present a new Curry-Howard correspondence for HA + EM_1, constructive Heyting Arithmetic with the excluded middle on \Sigma^0_1-formulas. We add to the lambda calculus an operator ||_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM_1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems.

TCS Journal 2012 Journal Article

Internal models of system F for decompilation

• Stefano Berardi
• Makoto Tatsuta

This paper considers Girard’s internal coding of each term of System F by some term of a code type. This coding is the type-erasing coding definable already in the simply typed lambda-calculus using only abstraction on term variables. It is shown that there does not exist any decompiler for System F in System F, where the decompiler maps a term of System F to its code. An internal model of F is given by interpreting each type of F by some type equipped with maps between the type and the code type. This paper gives a decompiler–normalizer for this internal model in F, where the decompiler–normalizer maps any term of the internal model to the code of its normal form. It is also shown that for any model of F the composition of this internal model and the model produces another model of F whose equational theory is below untyped beta–eta-equality.

CSL Conference 2012 Conference Paper

Knowledge Spaces and the Completeness of Learning Strategies

• Stefano Berardi
• Ugo de'Liguoro

We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy. We use a leading example to illustrate how non-constructive proofs lead to continuous and effective learning strategies over knowledge spaces, and prove that our learning semantics is sound and complete w. r. t. classical truth, as it is the case for Coquand's and Krivine's approaches.

CSL Conference 2011 Conference Paper

Non-Commutative Infinitary Peano Arithmetic

• Makoto Tatsuta
• Stefano Berardi

Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This system is unique among other non-commutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedent-grouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma-0-1 excluded middle.

I&C Journal 2009 Journal Article

Toward the interpretation of non-constructive reasoning as non-monotonic learning

• Stefano Berardi
• Ugo de’Liguoro

We study an abstract representation of the learning process, which we call learning sequence, aiming at a constructive interpretation of classical logical proofs, that we see as learning strategies, coming from Coquand’s game theoretic interpretation of classical logic. Inspired by Gold’s notion of limiting recursion and by the Limit-Computable Mathematics by Hayashi, we investigate the idea of learning in the limit in the general case, where both guess retraction and resumption are allowed. The main contribution is the characterization of the limits of non-monotonic learning sequences in terms of the extension relation between guesses.

CSL Conference 2008 Conference Paper

A Calculus of Realizers for EM1 Arithmetic (Extended Abstract)

• Stefano Berardi
• Ugo de'Liguoro

Abstract We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, which we call EM 1 -arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the “environment” and with each other. With respect to known constructive interpretations of classical arithmetic, the present one differs under many respects: for instance, the interpretation is compositional in a strict sense; in particular the interpretation of (the analogous of) the cut rule is the plain composition of functionals. As an additional remark, any two quantifier-free formulas provably equivalent in classical arithmetic have the same realizer.

TCS Journal 2008 Journal Article

Calculi, types and applications

• Stefano Berardi
• Ugo de’Liguoro

TCS Journal 2003 Journal Article

A full continuous model of polymorphism

• Franco Barbanera
• Stefano Berardi

We introduce a model of the second-order lambda calculus. Such a model is a Scott domain whose elements are themselves Scott domains, and in it polymorphic maps are interpreted by generic continous maps.

I&C Journal 1997 Journal Article

The Simply Typed Theory ofβ-conversion Has No Maximum Extension

• Franco Barbanera
• Stefano Berardi

It is proved that no maximum consistent extension exists for the simply typed theory ofβ-conversion.

I&C Journal 1996 Journal Article

A Symmetric Lambda Calculus for Classical Program Extraction

• Franco Barbanera
• Stefano Berardi

We introduce aλ-calculus with symmetric reduction rules and “classical” types, i. e. , types corresponding to formulas of classical propositional logic. The strong normalization property is proved to hold for such a calculus, as well as for its extension to a system equivalent to Peano arithmetic. A theorem on the shape of terms in normal form is also proved, making it possible to get recursive functions out of proofs ofΠ 0 2formulas, i. e. , those corresponding to program specifications.

I&C Journal 1991 Journal Article

Retractions on dI-domains as a model for Type:Type

• Stefano Berardi

We introduce an extension, with the Type: Type assumption, for a higher-order functional language, in the framework of λβp (the extension of the type-free lambda calculus introduced in R. Amadio and G. Longo (1986b, in “IFIP Conference ‘Formal Description of Programming Concepts, ’ Ebberup (DK), August 1986”)). Then, we find (using the stable functions and Berry's dI-domains) a model for λβp. This settles the consistency problem for λβp, up to now open, and gives very simple mathematical models for higher-order calculi with Type: Type. Such models are based on the relevant property that the range of a stable retraction on a dI-domain is still a dI-domain. Finally, we give the categorical description of the models of λβp, based on Moggi-Asperti's notion of internalization (in A. Asperti, 1988, “Models of Higher Order Calculi Internal Categories, ” Carnegie-Mellon report, in preparation).