arXiv subjects

Luca Tranchini

Publications and source records attributed to Luca Tranchini.

4 recordsLinked to original sources

arXiv2021

What's Decidable about (Atomic) Polymorphism

Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate System Fat, or atomic System F, a very weak predicative fragment of System F whose typable terms coincide with the simply typable ones. We show that the type-checking problem for Fat is decidable and we propose an algorithm which sheds some new light on the source of undecidability in full System F. Moreover, we investigate free theorems and contextual equivalence in this fragment, and we show that the latter, unlike in the simply typed lambda-calculus, is undecidable.

cs.LO↗

arXiv2019

The naturality of natural deduction

Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic $NI^2$. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of $NI^2$ is assumed to consist only of $β$ and $η$ equations. On the basis of the categorial interpretation of $NI^2$, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting $NI^2$-derivations. We show that the Russell-Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. We show that these result generalize some facts which have gone so far unnoticed, namely that the Russell-Prawitz translation maps particular classes of instances of the equations governing disjunction (and the other definable connectives) onto equations which are already included in the $βη$ equational theory of $NI^2$. Finally, we compare our approach with the one proposed by Ferreira and Ferreira and show that the naturality condition suggests a generalization of their methods to a wider class of formulas.

math.LO↗

arXiv2019

The naturality of natural deduction (II). Some remarks on atomic polymorphism

In a previous paper (of which this is a prosecution) we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models. In a recent series of papers a different approach to extract proof-theoretic properties of natural deduction derivations was proposed by defining predicative variants of the usual translation, embedding intuitionistic propositional logic into the atomic fragment of System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification provided by parametricity.

math.LO↗

arXiv2019

The Yoneda Reduction of Polymorphic Types (Extended Version)

In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than beta-eta-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to compute program equivalence in some fragments of System F.

cs.LO↗