Moderator: Type Systems of Programming Languages
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,
Okay, thank you.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.