Mini Workshop on Rewriting and Type Theory


Date: 3 October 2012
Place: Depto. de Computación, FCEyN, UBA. Room to be confirmed.
Contact information: com  gmail  eabonelli.

Program


 14:00 - 14:30 The Permutative Lambda-Calculus Beniamino Accattoli (Dept. of Computer Science, CMU)
 14:30 - 15:00 Predicative PTS with explicit substitutions and judgemental equality Miguel Pagano (FaMAF, UNC)
 15:00 - 15:30
Normalisation for Dynamic Pattern Calculi Carlos Lombardi (UNQ, UBA)
 15:30 - 15:50  Coffee Break  
 15:50 - 16:20 Hypothetical Logic of Proofs Gabriela Steren (UBA)
 16:20 - 16:50 Infinitary Normalization and the Loop Lemma Roel de Vrijer (Vrije Universiteit)
 16:50 - 17:10 The structural lambda-calculus Delia Kesner (PPS, Université Denis Diderot)

Predicative PTS with explicit substitutions and judgemental equality

In 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 Lambda-Calculus

We 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 sigma-equivalence and Moggi’s assoc-equivalence. We prove
confluence modulo the equations and preservation of beta-strong nor-
malisation (PSN) by means of an auxiliary substitution calculus. The
proof of confluence relies on M-developments, a new notion of develop-
ment for λ-terms.

Normalisation for Dynamic Pattern Calculi

The Pure Pattern Calculus (PPC) extends the Lambda Calculus, as
well as the family of algebraic pattern calculi with first-class
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 parallel-or-like,
non-sequential behaviour. Therefore, devising normalising
strategies for PPC to obtain well-behaved 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 leftmost-outermost strategy for
Lambda Calculus and is strictly finer than parallel-outermost.
The normalisation proof is based on the notion of *necessary set
of redexes*, a generalisation of the notion of needed redex
encompassing non-sequential 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 Proofs

The Logic of Proofs is a refinement 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 Lemma


Two 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 lambda-calculus

Inspired 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 XL-development. 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.