6
$\begingroup$

This question concerns the representation used in Arthur Charguéraud's paper “The locally nameless representation” and is somehow a follow-up on this question, where it is asked about the normalization of terms under a binder, at the example of the following term (for technical reasons, I use one based indices):

$$\lambda((\lambda\lambda(2 \; 1)) \; 1)$$

Beta-reductions in this representations supposedly (and contrary to the answer to the linked question) are done without need of introducing fresh variable names, because we can replace a variable opening + substitution combination

$$((\lambda \; t ) \; u) \longrightarrow_\beta [x \mapsto u] \; t^{x} \qquad (x \text{ fresh in } t)$$

by simple “term” opening

$$((\lambda \; t ) \; u) \longrightarrow_\beta t^{u},$$

where $t^{u} = \mathtt{open}(1, u, t)$ (see p. 10 in the paper). open can be implemented as follows, trying to exactly follow the definition there and Charguérot's reference implementation in Coq:

open k u (Bvar i)    = if k == i then u else (Bvar i)
open k u (Fvar x)    = Fvar x
open k u (Abs t1)    = Abs (open (k + 1) u t1)
open k u (App t1 t2) = App (open k u t1) (open k u t2)

Now, reducing the example term in (what I think is) normal order will result in the following steps:

\begin{align*} \mathtt{reduce}\; \lambda((\lambda\lambda(2 \; 1)) \; 1) &= \lambda(\mathtt{reduce} \; ((\lambda\lambda(2 \; 1)) \; 1)) \\ &= \lambda(\mathtt{open} \; 1 \; 1 \; (\lambda(2 \; 1))) \\ &= \lambda( \lambda (\mathtt{open} \; 2 \; 1 \; (2 \; 1))) \\ &= \lambda( \lambda ((\mathtt{open} \; 2 \; 1 \; 2) \; (\mathtt{open} \; 2 \; 1 \; 1))) \\ &= \lambda \lambda (1 \; 1) \end{align*}

This is, however, the wrong result -- the answer should have been $\lambda \lambda (2 \; 1)$ (essentially, just eta converting the term). The problem lies in the second-last line, where the bound $1$ from outside replaces the inner $2$ without being properly changed.

Appearently, open in this form is not made for normal order, due to the fact that unlike evaluation in de Bruijn representation, the substituted term is not shifted. In fact, I found the following comment on top of Charguéraud's implementation of open (called open_rec there):

We make several simplifying assumptions in defining [open_rec]. First, we assume that the argument [u] is locally closed. This assumption simplifies the implementation since we do not need to shift indices in [u] when passing under a binder. Second, we assume that this function is initially called with index zero and that zero is the only unbound index in the term. This eliminates the need to possibly subtract one in the case of indices.

Of course, the assumption of local closedness holds only when we do something like call-by-name, where terms under binders are not reduced. My solution was to change open to the following open', which “inlines” shifting of bound variables when they are inserted (which can be done easily, since we keep track of the number of binders anyway with k):

open' k (Bvar j) (Bvar i) = if k == i then (Bvar j + k - 1) else (Bvar i)
open' k u (Bvar i)    = if k == i then u else (Bvar i)
open' k u (Fvar x)    = Fvar x
open' k u (Abs t1)    = Abs (open' (k + 1) u t1)
open' k u (App t1 t2) = App (open' k u t1) (open' k u t2)

The questions I have are:

  • Is my reasoning correct?
  • Does open' correctly fix the problem when the assumptions do not hold (ie, when used in normal order reduction)?
  • Does open' preserve the properties and correctness of open when the original assumptions hold?
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.