## Recursion in lambda-calculus

Moderator: Type Systems of Programming Languages

timo.b
Mausschubser
Beiträge: 79
Registriert: 28. Sep 2009 16:18

### Recursion in lambda-calculus

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?

kind regards
Timo Bähr
Zuletzt geändert von timo.b am 6. Mär 2014 17:07, insgesamt 1-mal geändert.

cofi
Mausschubser
Beiträge: 86
Registriert: 22. Sep 2009 12:07

### Re: Recursion in lambda-calculus

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.

timo.b
Mausschubser
Beiträge: 79
Registriert: 28. Sep 2009 16:18

### Re: Recursion in lambda-calculus

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.