Mini Workshop on Rewriting and Type TheoryDate: 3 October 2012
Place: Depto. de Computación, FCEyN, UBA. Room to be confirmed.
Contact information: com gmail eabonelli.
Program
Predicative PTS with explicit substitutions and judgemental equalityIn this article we introduce a new formulation of PTSs with explicit
substitutions and prove the equivalence between two presentations of
PTSs that differ in their notion of conversion. One presentation is
more akin to MLTT where equality is defined by rules of the typing
system; the more common approach is to take equality as the
convertibility relation defined among raw terms. The former is known
as judgemental equality and is convenient for theoretical
considerations [11, 15]; the latter is known as external equality and
is often used in implementations like Coq and Matita. The proof of
the equivalence is interesting because it is based on a semantic
technique, cf. below for previous results, which we think can be used
for PTSs with rule (η). Moreover, our result concerns PTSs with
explicit substitutions; it is not clear that the equivalence can be
shown using the same syntactical methods used for PTSs where
substitution is external.
The Permutative LambdaCalculusWe introduce the permutative λcalculus, an extension of
λcalculus with three equations and one reduction rule for permuting
constructors, generalising many calculi in the literature, in particular
Regnier’s sigmaequivalence and Moggi’s assocequivalence. We prove
confluence modulo the equations and preservation of betastrong nor
malisation (PSN) by means of an auxiliary substitution calculus. The
proof of confluence relies on Mdevelopments, a new notion of develop
ment for λterms.
Normalisation for Dynamic Pattern CalculiThe Pure Pattern Calculus (PPC) extends the Lambda Calculus, as
well as the family of algebraic pattern calculi with firstclass
patterns, i.e. patterns can be passed as arguments, evaluated and returned as results. The notion of *matching failure* of PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies it with parallelorlike, nonsequential behaviour. Therefore, devising normalising strategies for PPC to obtain wellbehaved implementations turns out to be challenging. This talk focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmostoutermost strategy for Lambda Calculus and is strictly finer than paralleloutermost. The normalisation proof is based on the notion of *necessary set of redexes*, a generalisation of the notion of needed redex encompassing nonsequential reduction systems. This is joint work with with Eduardo Bonelli, Delia Kesner and Alejandro Ríos and was presented at RTA 2012. Hypothetical Logic of ProofsThe Logic of Proofs is a reﬁnement of modal logic S4 in which the
assertion \Box A is replaced by ⟦s⟧A whose intended reading is “s is a
proof of A”. We introduce the Hypothetical Logic of Proofs (HLP) with
a natural deduction formulation, and prove it to be as expressive as
LP. We then introduce a term assignment for HLP, using terms to
represent derivations and defining a notion of term reduction to
encode reduction of proofs. We show some of the challenges encountered
while proving Type Preservation ("type" being understood as both the
proven formula and the associated proof witness), and discuss the next
steps to be taken.
Infinitary Normalization and the Loop LemmaTwo notions of convergence in infinitary rewriting, strong and weak convergence, give rise to two different concepts of infinitary normalization. The two can be related by way of a cute lemma with a long history, but which, until recently, remained largely unnoticed: the Loop Lemma. The structural lambdacalculusInspired by a recent graphical formalism for λcalculus based on
Linear Logic technology, we introduce an untyped structural
λcalculus, called λj, which combines action at a distance with
exponential rules decomposing the substitution by means of weakening,
contraction and dereliction. Firstly, we prove fundamental properties
such as confluence and preservation of βstrong
normalisation. Secondly, we use λj to describe known notions of
developments and superdevelopments, and introduce a more general one
called XLdevelopment. Then we show how to reformulate Regnier’s
σequivalence in λj so that it becomes a strong bisimulation. Finally,
we prove that explicit composition or decomposition of substitutions
can be added to λj while still preserving βstrong normalisation.
