0
$\begingroup$

From Types and Programming Languages by Pierce

A term $t$ is in normal form if no evaluation rule applies to it— i.e., if there is no $t'$ such that $t -→ t'$.

and

A term $t$ is typable (or well typed) if there is some $T$ such that $t : T$.

In the pure simple typed lambda calculus:

we consider another fundamental theoretical property of the pure simply typed lambda-calculus: the fact that the evaluation of a well- typed program is guaranteed to halt in a finite number of steps—i.e., every well-typed term is normalizable.

Does a term being normalizable mean the same as the term has a normal form?

Here is a term which has no normal form in the untyped lambda calculus:

Recall that a term that cannot take a step under the evaluation relation is called a normal form. Interestingly, some terms cannot be evaluated to a nor- mal form. For example, the divergent combinator

$$omega = (λx. x x) (λx. x x);$$

contains just one redex, and reducing this redex yields exactly omega again! Terms with no normal form are said to diverge.

In the pure simple typed lambda calculus,

  • is $omega$ typable (i.e. well-typed)?
  • is $omega$ normalizable?
  • does $omega$ have a normal form?
$\endgroup$
1
$\begingroup$

Yes, a term is normalizable if, and only if, it has a normal form.

It is well known that $\omega = (\lambda x . x x) (\lambda x . x x)$ is not typeable, nor is it normalizable. It is not normalizable because it has an evaluation step ($\beta$-reduction) which evaluates it to itself, so we get $\omega \mapsto \omega \mapsto \omega \cdots$.

To see that it is not typeable, observe that already its subexpression $\lambda x . x x$ is not typeable. For if $x$ has type $T$ then in order for $x x$ to have a type, $T$ must be of the form $T \equiv T \to S$ (because $x$ is applied to something, therefore by the typing rules it must have a function type). But there is no type $T$ such that $T \equiv T \to S$, because the type on the right-hand side is larger (as a syntactic expression) than the type on the left-hand side.

| cite | improve this answer | |
$\endgroup$

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.