Of course you can. Use the Y-combinator.
This would look cleaner if the author had not used Church numerals. Here's something simpler:
(λf λn. if n=0 then 1 else n*f(n-1) ) (λf λn. if n=0 then 1 else n*f(n-1)) 6.
But this isn't quite right, since recursion stops after one step. The Y combinator is more devious even than this.
So the factorial function is: Y (λf λn. if n=0 then 1 else n*f(n-1) ).
See section 7 of this PDF for a worked example.
---
(Of course the Church Numerals were used to encode "if n=0 then 1.."".)
ReplyDeleteThis is actually an apt posting which should relate to the remarks I made a couple of blog posts ago. The first point of contact is the Curry Paradox mentioned in the Y combinator Wikipedia article, and the conclusion that the Lambda calculus is inconsistent as a
deductive system.
This leads to various discussions as to why and in what way, and generally the larger question of "how does (raw) computation theory mess with our traditional (and deductive) notions of logic?" - and does that have yet wider implications in our deductive sciences....
More blog posts required...
You may recall this was the motivation for Scott–Strachey denotational semantics with its emphasis on lattices and fixed points.
DeleteYes, however the Scott-Strachey denotational semantics is to some extent still "work in progress". Especially for topics of computational generality like concurrency and the appropriateness and meaning of the logics involved. Apprarently the first fully abstract formulation of Plotkin's PCF was done using Game Semantics in the 2000s (according to WikiP).
DeleteIn particular the associated logics are not usually classical, are they? Undecidability results tend to get in the way of clean logical statements in this area, preventing a "big picture" from easily being formed.