3
$\begingroup$

I heard that untyped lambda expressions can have no normal forms. As an example, the expression $(\lambda x. x\space x) (\lambda x. x\space x)$ , when put to a $\beta$ conversion, gives back the same expression. I can see that this is truly a problem because the term rewriting never ends.

On the other hand, proof assistants such as J-Bob are based on lisp/scheme expressions, which seem to be untyped lambda calculus. I am not sure about ACL2, but the name suggests that it is based on lisp expressions.

My questions are:

Are there other types of lambda expressions without normal forms that can cause troubles for proof assistants?

If the above mentioned proof assistants are really based on untyped lambda calculus, what mechanism is used in such proof assistants to deal with cases where there is no normal forms?

$\endgroup$
3
  • $\begingroup$ I don't think the title of your question reflects the content. In fact you seem to answer your own question in the first paragraph: $(\lambda x.x\ x)(\lambda x. x \ x)$ doesn't have a normal form because 1) it's not normal, and 2) it reduces to itself. $\endgroup$
    – Couchy
    Dec 4, 2022 at 21:24
  • $\begingroup$ I think it's important to separate Lisp syntax i.e. s-expressions, from the type system of Scheme or Common Lisp or Racket etc. Just because the underlying syntax is like Lisp doesn't mean the type system is, and even if you elaborate to an untyped language, you can implement types and dependent types as macros. So being embedded in Lisp does not mean being an untyped lambda calculus. $\endgroup$ Dec 6, 2022 at 17:16
  • $\begingroup$ Just because you don't have normalization doesn't mean you don't have equivalence. You just have to manually prove two terms equivalent. It is certainly very inconvenient though. $\endgroup$ Dec 7, 2022 at 1:10

1 Answer 1

2
$\begingroup$

Firstly, for general recursion in the lambda calculus you need the Y-combinator:

$$Y = \lambda f.(\lambda x.f (x\ x)) (\lambda x.f (x\ x))$$ which satisfies $Y\ g = g\ (Y\ g)$. But in general you can't decide whether a term containing Y terminates.

In practice however, languages don't explicitly use the Y combinator and instead use some internal form of evaluation.

I don't know about J-bob, but ACL2 actually doesn't allow lambda expressions, since terms are first order, so you can neither define the expression you describe (the $\Omega$ combinator), nor the Y combinator. Instead when you define a recursive function ACL2 requires you provide a measure on the arguments which decreases on each recursive call. Usually this can be proved automatically because ACL2 guesses a measure:

> (defun foo (x) (if (consp x) (1+ (foo (cdr x))) 0))

The admission of FOO is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of FOO is described by the
theorem (AND (INTEGERP (FOO X)) (<= 0 (FOO X))).  We used primitive
type reasoning.
$\endgroup$
2
  • $\begingroup$ thanks. I understand it better now. lambda expressions cannot be used as values/terms in ACL2/J-Bob. By using lambda expression, I was thinking about untyped lambda functions such as (defun i (x) (x x)) (defun j (x) ((i x) (i x))). Also, I have the impression that theorems are represented as boolean valued functions that always returns true, right? So, when a theorem is proved, is it represented as a untyped lambda function somewhere? $\endgroup$
    – tinlyx
    Dec 5, 2022 at 1:51
  • $\begingroup$ No, both theorems and functions are represented as terms with free variables. Theorems are interpreted as functions whose value is known to be non nil $\endgroup$
    – Couchy
    Dec 5, 2022 at 5:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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