Hard problems

Lambda calculus was created by Alonzo Church in the early 1930's.  This tiny logic is turing complete.  In fact, it was turing complete before turing completeness was a thing.  Alonzo Church published his lambda calculus shortly before Alan Turing published his work with turing machines.  

Every computable function is computable in a system which is turing complete.  And what this means for lambda calculus is, basically, anything you can do in math you can represent in lambda calculus.  However, originally, Alonzo Church was having some problems making lambda calculus do everything.  He was having problems making it do a very simple function.  The predecessor function.  Or in other words ... subtract one from a number.

The story goes that Church thought about it very hard and was considering giving up on lambda calculus when his student, Stephen Kleene, went to the dentist.  There Kleene reasoned out a way to implement the predecessor function by using triples (a list with exactly three items).  The more modern version uses pairs.  

So here's the point.  Alonzo Church was smart enough to come up with lambda calculus in the first place.  This is a system which is powerful enough to describe everything that we are capable of formally describing.  But he wasn't smart enough to figuring the missing piece that would make basic subtraction work.  That was solved by Kleene.  Additionally, it's not like Kleene just walked in and solved the thing.  He was clearly thinking about it very hard.  So hard in fact that he was thinking about it even when he was off at the dentist.

Solving truly hard problems isn't a question of raw intelligence.  Church was clearly very intelligent.  And it's also not a question of just putting in the hours.  Kleene solved the predecessor function while he was on a personal errand.  

If you're working on a truly hard problem, you might not be able to solve it.  And this is regardless of how smart you are.  Additionally, there isn't a set algorithm for coming up with the solution.



I once tried to come up with the solution to the predecessor function on my own.  I almost got there without cheating, but in the end I checked around online.  Had I known that the predecessor function was so difficult to originally come up with, I probably would have worked harder to solve it on my own.  Although I would have still been cheating.  Because I knew that it was actually possible to solve.

This is the solution that I found that I was able to actually understand in the end.  It took a lot of work to figure out, but my intutition was correct.  My idea was that you needed to "unwrap the number" and then just "rewrap" it one less time than it's original total.  [In lambda calculus numbers are typcially represented as a number of times that you do something else.  Unwrapping a number is cognatively similar to unwrapping a loop as an optimization techique.  Except you're not in it for the optimization.]

0 = λ f . λ v . v
1 = λ f . λ v . f v
2 = λ f . λ v . f ( f v )

pred = λ n . λ f . λ v . n ( (λ a . λ b . b ( a f ))  (λ u . v)  (λ i . i) )