arXiv subjects
Publications and source records attributed to Delia Kesner.
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.
Multi types---aka non-idempotent intersection types---have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps. Starting from this observation, we refine and generalise a technique introduced by Bernadet & Graham-Lengrand to provide exact bounds for the maximal strategy. Our typing judgements carry two counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the lambda-calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation). Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy---the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure---and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A.Melliès in his PhD thesis. The theorem states that multistep strategies reducing so called necessary and never-gripping sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behavior of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.
This document contains the proceedings of the Seventh International Workshop on Logical and Semantic Frameworks, with Applications, which was held on September 29 and 30, 2012, in Rio de Janeiro, Brazil. It contains 11 regular papers (9 long and 2 short) accepted for presentation at the meeting, as well as extended abstracts of invited talks by Torben Braüner (Roskilde University, Denmark), Maribel Fernández (King's College London, United Kingdom), Edward Hermann Haeusler (PUC-Rio, Brazil) and Alexandre Miquel (École Normale Supérieure de Lyon, France).
Inspired by a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda j, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and derelicition. First, we prove some fundamental properties of lambda j such as confluence and preservation of beta-strong normalisation. Second, we add a strong bisimulation to lambda j by means of an equational theory which captures in particular Regnier's sigma-equivalence. We then complete this bisimulation with two more equations for (de)composition of substitutions and we prove that the resulting calculus still preserves beta-strong normalization. Finally, we discuss some consequences of our results.
This work gives some insights and results on standardisation for call-by-name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern. We prove the Standardisation Theorem by using the technique developed by Takahashi and Crary for lambda-calculus. The proof is based on the fact that any development can be specified as a sequence of head steps followed by internal reductions, i.e. reductions in which no head steps are involved.
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.