Seite 1 von 1

Recursion in lambda-calculus

Verfasst: 6. Mär 2014 16:52
von timo.b
Hi,

in the full (untyped) lambda-calculus it seems to be possible to write recursive functions like a recursive implementation of a factorial function. For instance in the Pierce book they were able to evaluate the result of \(factorial\:3\) by using a fix-point combinator (page 67).

Do we have discussed the full lambda-calculus in the lecture? Are there any restrictions in our (untyped) lambda-calculus?

As far as I remember, we were not able to type recursive terms. Does the problem occurs when typing such a term or before?

Thank you for an answer,
kind regards
Timo Bähr

Re: Recursion in lambda-calculus

Verfasst: 6. Mär 2014 17:07
von cofi
We wrote general recursive functions using a fixpoint combinator in the untyped lambda calculus, see Assignment 4.
Our problems only started when we moved on to the simply typed calculus because we could not - as you said - type the fixpoint combinator.

Re: Recursion in lambda-calculus

Verfasst: 6. Mär 2014 17:08
von timo.b
cofi hat geschrieben:We wrote general recursive functions using a fixpoint combinator in the untyped lambda calculus, see Assignment 4.
Our problems only started when we moved on to the simply typed calculus because we could not - as you said - type the fixpoint combinator.
Okay, thank you.