arXiv subjects

Simona Ronchi Della Rocca

Publications and source records attributed to Simona Ronchi Della Rocca.

12 recordsLinked to original sources

arXiv2026

Principal Typing for Intersection Types, Forty-Five Years Later

A type assignment system for lambda-calculus enjoys the principal typing property if every typable term M has a special typing, called principal, from which all typings for M can be obtained via suitable operations. The existence of principal typings in various intersection type disciplines has long been established using both semantical and syntactical approaches. Historically, on the syntactical side, proofs of this property and the description of type inference (semi-)algorithms computing principal typings have been complicated by many subtle technicalities; the present work aims at providing a more accessible formulation. To this end, we revisit some classical notions, and identify three elementary operations (substitution, expansion, erasure) that allow to build any type derivation in a system characterizing head normalization. We then use such operations in the design of an inference semi-algorithm that computes the principal typing of all and only the strongly normalizing terms, thus contributing to a modern perspective on results originally proven more than 40 years ago

cs.LO↗

arXiv2026

Strong normalization through idempotent intersection types: a new syntactical approach

It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems rely on semantical techniques. In this work, we study $Λ_\cap^e$, a variant of Coppo and Dezani's (Curry-style) intersection type system, and we propose a syntactical proof of strong normalization for it. We first design $Λ_\cap^i$, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in $Λ_\cap^i$ implies SN through a measure that, given a term, produces a natural number that decreases along with reduction. Finally, the result is extended to $Λ_\cap^e$, since the two systems simulate each other.

cs.LO↗

arXiv2021

Solvability = Typability + Inhabitation

We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabitation in an intersection type system P based on non-idempotent types. We show first that the system P characterizes the set of terms having canonical form, i.e. that a term is typable if and only if it reduces to a canonical form. But the set of solvable terms is properly contained in the set of canonical forms. Thus, typability alone is not sufficient to characterize solvability, in contrast to the case for the lambda-calculus. We then prove that typability, together with inhabitation, provides a full characterization of solvability, in the sense that a term is solvable if and only if it is typable and the types of all its arguments are inhabited. We complete the picture by providing an algorithm for the inhabitation problem of P.

cs.LO↗

arXiv2020

Intersection Types and (Positive) Almost-Sure Termination

Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of obtaining any given result, rather than the possibility or the necessity of obtaining it, like in (non)deterministic computation. Termination, arguably the simplest kind of reachability problem, can be spelled out in at least two ways, depending on whether it talks about the probability of convergence or about the expected evaluation time, the second one providing a stronger guarantee. In this paper, we show that intersection types are capable of precisely characterizing both notions of termination inside a single system of types: the probability of convergence of any lambda-term can be underapproximated by its type, while the underlying derivation's weight gives a lower bound to the term's expected number of steps to normal form. Noticeably, both approximations are tight -- not only soundness but also completeness holds. The crucial ingredient is non-idempotency, without which it would be impossible to reason on the expected number of reduction steps which are necessary to completely evaluate any term. Besides, the kind of approximation we obtain is proved to be optimal recursion theoretically: no recursively enumerable formal system can do better than that.

cs.LO↗

arXiv2018

Inhabitation for Non-idempotent Intersection Types

The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the decidability of the inhabitation problem for all the systems considered, by providing sound and complete inhabitation algorithms for them.

cs.LO↗

arXiv2017

Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characterizations of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin's one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin's call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi's approach of parallel reductions to our set of reduction rules. The standardization is weak (i.e. redexes are not fully sequentialized) because of overlapping interferences between reductions.

cs.LO↗

arXiv2014

A type assignment for lambda-calculus complete both for FPTIME and strong normalization

One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of computer science. One of the more promising approaches to this aim is based on the use of lambda-calculus as paradigmatic programming language and the design of type assignment systems for lambda-terms, where types guarantee both the functional correctness and the complexity bound. Here we propose a system of stratified types, inspired by intersection types, where intersection is a non-associative operator. The system, called STR, is correct and complete for polynomial time computations; moreover, all the strongly normalizing terms are typed in it, thus increasing the typing power with respect to the previous proposals. Moreover, STR enjoys a stronger expressivity with respect to the previous system STA, since it allows to type a restricted version of iteration.

cs.LO↗

arXiv2013

Bounding normalization time through intersection types

Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.

cs.LO↗

arXiv2012

Standardization in resource lambda-calculus

The resource calculus is an extension of the lambda-calculus allowing to model resource consumption. It is intrinsically non-deterministic and has two general notions of reduction - one parallel, preserving all the possible results as a formal sum, and one non-deterministic, performing an exclusive choice at every step. We prove that the non-deterministic reduction enjoys a notion of standardization, which is the natural extension with respect to the similar one in classical lambda-calculus. The full parallel reduction only enjoys a weaker notion of standardization instead. The result allows an operational characterization of may-solvability, which has been introduced and already characterized (from the syntactical and logical points of view) by Pagani and Ronchi Della Rocca.

cs.LO↗

arXiv2011

Intersection Logic in sequent calculus style

The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.

cs.LO↗

arXiv2010

An Implicit Characterization of PSPACE

We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STAB is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.

cs.LO↗

arXiv2008

Light Logics and the Call-by-Value Lambda Calculus

The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we show that shifting from usual call-by-name to call-by-value lambda calculus allows regaining strong connections with the underlying logic. This will be done in the context of Elementary Affine Logic (EAL), designing a type system in natural deduction style assigning EAL formulae to lambda terms.

cs.LO↗