# Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression

In this question, I am talking about the language Pie described in the book The Little Typer.

Consider the definition

(claim foo-or-bar (-> Nat Atom Atom))
(define foo-or-bar
(λ (n) (ind-Nat n
(λ (n) (-> Atom Atom))
(λ (a) 'foo)
(λ (n-1 result_n-1 a) 'bar))))


If I then type foo-or-bar on a separate line and execute, Pie outputs

(the (→ Nat Atom
Atom)
(λ (n x₁)
((ind-Nat n
(λ (n₁)
(→ Atom
Atom))
(λ (a)
'foo)
(λ (n-1 result_n-1 a)
'bar))
x₁)))


So, Pie says that the second code snippet is the normal form of foo-or-bar. It's pretty clear why

(λ (n x₁)
((ind-Nat n
(λ (n₁)
(→ Atom
Atom))
(λ (a)
'foo)
(λ (n-1 result_n-1 a)
'bar))
x₁))


is the same (-> Nat Atom Atom) as

(λ (n) (ind-Nat n
(λ (n) (-> Atom Atom))
(λ (a) 'foo)
(λ (n-1 result_n-1 a) 'bar)))


It's by The Final Second Commandment of lambda, which says

If f is a (Pi ((y Y)) X), and y does not occur in f, then f is the same as (lambda (y) (f y)).

But The Little Typer say that the normal form of an expression is the most direct way of writing it. And, frankly, what I wrote in the definition of foo-or-bar seems more direct than what Pie says its normal form is. So, why is that the normal form? I remember the book said somewhere that if f is a neutral expression of a Pi type, then (lambda (x) (f x) is the normal form of f. This seems similar to the situation with foo-or-bar but not directly applicable.

There are 2 questions here.

The first one is whether the situation is applicable. In fact it is! This is because $$(\lambda (x\ y)\ f)$$ is abbreviation for $$(\lambda (x)\ (\lambda (y)\ f))$$. So you apply that in the inner layer.

The second question is why $$(\lambda (x)\ (f\ x))$$ is more "direct" than $$f$$. This is because $$\lambda$$ is the only way to create a $$\Pi$$ type. Thus it would be more direct to explicitly convey this knowledge. Remember that "direct" doesn't mean short or concise. For example, 10000000000 is a much more direct way to write $$10^{10}$$ but it is much longer.

The Little Typer chose to use a more blurry definition. But in practice it is well-defined. Only when the type is $$\mathbb N, A+B, \mathcal U$$, should a neutral term of that type be normal.

• I think I understand now. If n is a variable of type Nat, and thus a neutral expression, is (ind-Nat n (λ (n) (-> Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar))) a neutral expression? Yes, by the box "Neutral expressions" in ch. 8. What is its type? Its type is (Pi ((a Atom)) Atom. What is its normal form? Its normal form is (lambda (a) ((ind-Nat n (λ (m) (-> Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar))) a). It's considered simpler and more direct because it's not neutral, instead it's a value, I would guess. Sep 4, 2022 at 22:19
• If e is a type and G is an expression which is a type whenever e is a type, and f is a variable of type (Pi ((x e)) G), why is (lambda (x) ((lambda (y) (f y)) x))  not the normal form of (lambda (y) (f y))? Because (lambda (y) (f y)) is not a neutral expression. Sep 4, 2022 at 22:28
• Why can a neutral expression of one of the types Nat, A+B ,U be normal? I would guess that it can be normal because those three types have multiple constructors, so if the expression is neutral, then we don't know which constructor was used. But can a neutral expression of the type Atom be normal? Sep 4, 2022 at 22:35
• If I write (the (-> (-> Atom Atom) (-> Atom Atom)) (λ (f) f)) in Pie, it outputs (the (→ (→ Atom Atom) Atom Atom) (λ (f x₁) (f x₁))). I think this means that the type Atom should also be added to your list of three special types. Sep 4, 2022 at 22:51
• @CrabMan Quite. I forgot there is an Atom type. It is actually special because it is not defined by a universal property (i.e. it doesn't have an eliminator). So the definition of normal/neutral can bend a bit. For example you can consider an atom to be neutral. It doesn't break the theory.
– Trebor
Sep 5, 2022 at 3:57