[TYPES] Typed lambda calculi with weak conversion

[Gabriel Scherer]

# Çağman and Hindley's notion of weak reduction

For those that would not be familiar with the work of Çağman and Hindley,
1998 (it is a nice paper that is still readable today, so don't hesitate to
have a look), they give a definition of weak reduction (as opposed to
strong/full reduction) that is a bit stronger (and arguably better-behaved)
than the standard one: instead of saying "don't reduce under lambdas", they
say "only reduce closed term" -- this is essentially the same thing, except
that they allow themselves to reduce closed sub-terms that would occur
under a lambda. For example:

  (lam y. (lam x. x) (lam z. z))

would not reduce for the common notion of weak reduction ((lam y . []) is
not an evaluation context), but it does reduce to

  (lam y. (lam z. z))

for their notion of weak reduction. (Luc Maranget once claimed to me that
this is the "right" notion of weak reduction.)

One nice idea in the paper of Çağman and Hindley is that this can be
characterized very nicely by using the no-variable-capture property of
substitutions (as opposed to context plugging). Strong/full reduction can
be defined by saying that, for any head-reduction from A to B (a "head"
reduction is when A is the redex, instead of merely containing the redex as
a subterm; if you only have functions, this is when A is of the form ((lam
x. C) D)):

  C[A] reduces to C[B]

for an arbitrary context C. (Just a term with a hole, no particular
restriction to a family of evaluation contexts). Çağman and Hindley remark
that their notion of weak reduction can be characterized by saying that,
for any head-reduction from A to B,

  C[A/x] reduces to C[B/x]

using (capture-avoiding) substitution instead of context plugging imposes
that A and B do not contain a variable bound in C, which precisely
corresponds to their notion of weak reduction.
(Consider (lam y . z) and (lam y . y), the former can be written as (lam y
. x)[z/x], but the latter is not equal to (lam y . x)[y/x].)

# Normalization of weak reduction

To answer Filippo's question: I don't think that enlarging the notion of
weak reduction to reduce closed subterms changes the normalization behavior
in any way: the two notions of weak reduction have the same normalization
properties.

In particular, consider a term of the form

  C[A]

where A is a closed sub-term in the sense that is under some lambdas in C,
but does not use their bound variables. A is not reducible under the
no-reduction-under-lambda interpretation (the common one), but it is
reducible under the reduce-closed-subterms interpretation (Çağman and
Hindley's -- let's call it "CH weak reduction" for short). But this term is
beta-equivalent to

  (lam x. C[x]) A

where A is in reducible position under either notions of reductions. If
C[A] was non-normalizable for CH weak reduction, then ((lam x. C[x]) A) is
non-normalizable for standard weak reduction. If the standard calculus has
a weak-normalization property, then you know that Ch-reducing A in C[A]
preserves normalization.

My intuition suggests that this can be turned a general construction that
extrudes all closed sub-term of a term, and produces from any term T an
extruded term T' such that the CH-weak normal form of T is the standard
normal form of T'. (Of course, this is only intuition, one has to do the
work.) (This extrusion is type-preserving.) This means that any
normalization result for standard weak reduction implies a normalization
result for CH weak reduction.


# Explicit substitutions

I believe that CH-weak reduction is may be related to calculi with explicit
substitutions.
CH-weak reduction is "more confluent" than standard reduction, as reducing
(lam x. A) B preserves the property that B is in reducible position. (This
is not true of standard weak reduction, consider the case where A is (lam y
. C)). This property that head reduction preserves reducibility of their
subterms also holds for explicit substitution calculi.

On Sun, Feb 25, 2018 at 12:06 PM, Filippo Sestini <sestini.filippo at gmail.com
> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear all,
>
> The notion of weak reduction first appeared in [1], and was later
> developed into the definition of a weak lambda calculus in, for
> example, [2]. The crucial property of weak reduction is that it
> does not validate the ξ rule, but some form of computation under
> binders is still possible.
>
> I'm looking for references in the literature treating typed
> calculi with full lambda syntax and weak conversion, in
> particular regarding normalization. What I've found so far seems
> to either be limited to a form of combinator syntax, or only
> consider evaluation to weak head normal form ([3], [4]).
> Do you have any suggestions?
>
> Thank you
>
> Sincerely
>
> [1] W.A. Howard, Assignment of Ordinals to Terms for Primitive
> Recursive Functionals of Finite Type, 1970
> 1970
>
> [2] N. Çağman, J.R. Hindley, Combinatory weak reduction in lambda
> calculus, 1998
>
> [3] P. Martin-Löf, An Intuitionistic Theory of Types: Predicative
> Part, 1975
>
> [4] T. Coquand, P. Dybjer, Intuitionistic Model Constructions and
> Normalization Proofs, 1998
>
> --
> Filippo Sestini
> sestini.filippo at gmail.com
> (+39) 333 6757668
>
>