Writing a prime number generator in lambda calculus, starting from first principles.
So many way to play inside the good old holy world of lambda-calculus! The following document: http://jwodder.freeshell.org/lambda.html is a must have as a basis for many explorations.
Years ago I was looking for a small lambda-calculus evaluator working in a web browser - I really need to write living code in a web page - and here are some tests where I look for the shortest way, the simplest way, the "first principles", for example to build the numbers, the operators. Never satisfied, always searching:
http://lambdaway.free.fr/lambdawalks/?view=lambdacalc
http://lambdaway.free.fr/lambdawalks/?view=lambda_calculus
http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy
http://lambdaway.free.fr/lambdawalks/?view=coding
with the ultimate goal of having a programming language that can be used to compute primes, factorials, fibonaccis, a Fast Fourier Transform, ... or simply compose a web page. More in http://lambdaway.free.fr/lambdawalks/
I would be interested in your opinion.
> where I look for the shortest way, the simplest way, the "first principles", for example to build the numbers, the operators
Since the "conditional's" or implication's elimination (application-"MP"), introduction (abstraction) & distributivity axioms ("K" & "S") in addition to first binding a "hypothesis" or (free) variable "x", which is "f" in the "Iota" definition, leads to the "X" single combinator/axiom, and since "S" may be derived from ("B":local consistency) & ("K":local completeness or η-reduction (eta reduction) or extensionality) this leads to the shorter locally indecisive single aXiom definition := λx. x B K
Meredith first found a form of the shortest definition and others have been listed by the now deceased Dolph Ulrich: https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page...
A positive answer to QUESTION V (https://web.ics.purdue.edu/~dulrich/Twenty-six-open-question...) would seem to mean λx. x B K is as short as possible.
Is it so hypothetical? I'd have thought that function composition fits the Barbara syllogism.
Thanks for your reply.
I like your work, especially in how far you took it from "first principles".
What strikes me is your insight wrt calculating factorials based on Church numbers and pairs only, no control structures (except iteration using Church numbers). It helps placing the magic into perspective.
I had a similar experience implementing the (sound) reduction of the Y-combinator. Not so magic at all. Merely a trick for passing on the function for a recursive call.