1
$\begingroup$

Context

I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $\to_\beta$ I denote the $\beta$-reduction as a relation.

Also, my question eventually will use this $\lambda$-calculus with explicit substitution (originally called $\lambda\sigma$-calculus), where substitution is introduced on term level via closures $M[s]$ with $\lambda$-term M and substitution $s$.

A few definitions are needed.

Definition: Normal Form

A $\lambda$-term $M$ is in normal form, if there is no $\lambda$-term $N$ such that $M\to_\beta N$.

Besides this defintion, there is also another definition I'm ultimately interested in: defining normal form recursively:

Definition II: Neutral and Normal Form

Mutually defining neutral and normal forms:

Neutral Form:

  • Every variable is in neutral form.
  • if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.

Normal Form:

  • If $M$ is in neutral form, then $M$ is in normal form.
  • If $M$ is in normal form, then $\lambda M$ is in normal form.

Question

So far, this deals with the classical simply typed lambda calculus, where substitution is defined as a (meta-) function over terms. First: does this definition of normal forms make sense?

Then: Putting substitution into the term level, the question arises how to define normal forms then recursively as above?

Own Ideas

My first go to was to add the following case to the definition of a normal form:

  • If every term in $s$ is in neutral form and $t$ is in normal form, then $t[s]$ is in normal form.

Since neutral forms don't allow abstractions, even when dealing with closures like $(x y)[s]$, this should not introduce new $\beta$-redexes. But somehow, I'm unsure. Does this still resemble what NF means? After searching for information, there seems to be nothing like this.

$\endgroup$
  • $\begingroup$ Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas. $\endgroup$ – frabala Mar 16 at 14:53
  • $\begingroup$ Well, if they are normal, then consider $s = [x \leftarrow \lambda M, y\leftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed. $\endgroup$ – aphorisme Mar 16 at 14:56
  • $\begingroup$ I don't see a redex in $(x\, y)[x\leftarrow\lambda M, y\leftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x\, y)[x\leftarrow t_1, y\leftarrow t_2]$ reducing to $(t_1 y)[y\leftarrow t_2]$? $\endgroup$ – frabala Mar 16 at 15:04
  • $\begingroup$ Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((\lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in. $\endgroup$ – aphorisme Mar 16 at 15:07
  • $\begingroup$ You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is. $\endgroup$ – frabala Mar 16 at 15:56
1
$\begingroup$

Does the recursive definition make sense?

I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,

  1. if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
  2. if it has at least one redex, then it is not in II-normal form* and it's also not neutral.

There we go:

  • If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
  • If $t$ is a lambda $\lambda M$, then
    • if $M$ has no more redexes, then $\lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $\lambda M$ is also in II-normal form.
    • if $M$ contains at least one more redex, then $\lambda M$ also contains at least one and therefore we need to show (2). We easily see that $\lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $\lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $\lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $\lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
  • If $t$ is an application $M\,N$, we separate cases again:
    • If $M$ and $N$ contain no more redexes, it is still possible for $M\,N$ to be a redex. It is a redex, if $M$ is a lambda term $\lambda M'$ and, therefore, $t$ is of the form $\lambda M'\, N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $\lambda M'\,N$ is neutral if $\lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = \lambda M'\, N$ is not in II-normal form.
    • If $N$ or $M$ contain at least one redex, then $M\,N$ also does, so we need to show (2). Again we will assume $M\,N$ is in II-normal form and reach a contradiction. Since $M\,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M\,N$ is not in II-normal form.

This proves that Definition II is equivalent to "is $\beta$-irreducible".

How to adapt Definition II to also account for substitution terms $t[s]$?

By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?


*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"

$\endgroup$
  • $\begingroup$ I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue. $\endgroup$ – aphorisme Mar 16 at 16:10
  • $\begingroup$ @aphorisme, Appreciated :) $\endgroup$ – frabala Mar 16 at 16:12

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.