4 ms·

Tiny Prime Combinations

15 points by Suskewiet 4y ago

Suskewiet 4y ago
Writing a prime number generator in lambda calculus, starting from first principles.
- martyalain 4y ago
  Hi Suskeviet, So many way to play inside the good old holy world of lambda-calculus! The following document: http://jwodder.freeshell.org/lambda.html 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=lambdacalc http://lambdaway.free.fr/lambdawalks/?view=lambda_calculus http://lambdaway.free.fr/lambdawalks/?view=lambda_calculus http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=coding 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/ http://lambdaway.free.fr/lambdawalks/ I would be interested in your opinion.
  - l- 4y ago
    Regarding http://jwodder.freeshell.org/lambda.html http://jwodder.freeshell.org/lambda.html, "B" is Hypothetical Syllogism (transitivity of implication (the "material conditional")), which is the composition of the arguments x and y applied to the argument z (https://en.wikipedia.org/wiki/B,_C,_K,_W_system https://en.wikipedia.org/wiki/B,_C,_K,_W_system) rather than the composition of the arguments x and y alone. > 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.htm 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-questions-page.htm https://web.ics.purdue.edu/~dulrich/Twenty-six-open-question...) would seem to mean λx. x B K is as short as possible.
    - tempodox 4y ago
      > "B" is Hypothetical Syllogism Is it so hypothetical? I'd have thought that function composition fits the Barbara syllogism.
      - l- 4y ago
        Barbara & the other (categorical) https://en.wikipedia.org/wiki/Syllogism https://en.wikipedia.org/wiki/Syllogism take the "existential viewpoint" (see introduction on https://en.wikipedia.org/wiki/Categorical_proposition https://en.wikipedia.org/wiki/Categorical_proposition) that involves "term": https://en.wikipedia.org/wiki/Term_logic https://en.wikipedia.org/wiki/Term_logic instead of just "sentential": https://en.wikipedia.org/wiki/Propositional_calculus https://en.wikipedia.org/wiki/Propositional_calculus logic. From https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... the universal quantification "all" in Barbara corresponds to the generalized product (conjunction rather than implication) type. B is also known as the composition combinator & (implicational) forms are shown here: https://en.wikipedia.org/wiki/Hypothetical_syllogism#Alternative_forms https://en.wikipedia.org/wiki/Hypothetical_syllogism#Alterna...
  - Suskewiet 4y ago
    Alain, 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.
tromp 4y ago
A much more concise prime number generator in lambda calculus [1] [2] is λ (λ 1 (1 ((λ 1 1) (λ λ λ 1 (λ λ 1) ((λ 4 4 1 ((λ 1 1) (λ 2 (1 1)))) (λ λ λ λ 1 3 (2 (6 4))))) (λ λ λ 4 (1 3))))) (λ λ 1 (λ λ 2) 2) or in graphical notation [3] ───────────────────────────────────────────────── ┬─┬───────────────────────────────────┬──── ────┬ │ │ ┬─┬ ────┬─┬────────────────────── ┼───┬ ┬───┼ │ │ └─┤ ────┼─┼───────────────────┬── ┼───┼ │ ┬ │ │ │ │ ┬───┼─┼───────────────────┼── ┼─┬─┼ │ ┼ │ │ │ │ │ ─ ┼─┼─┬─────┬──── ──────┼─┬ │ ├─┘ └─┤ │ │ │ │ │ ┬ └─┤ │ ┬─┬ ┼─┬─┬ ──┬───┼─┼ ├─┘ ├─┘ │ │ │ └─┤ └─┤ └─┤ │ ├─┘ ──┼─┬─┼─┼ │ │ │ │ │ │ │ │ ├─┘ ┬─┼─┼─┼─┼ │ │ │ │ │ │ │ ├─┘ └─┤ │ ├─┘ │ │ │ │ │ │ └───┤ │ ├─┘ │ │ │ │ │ │ │ ├─┘ │ │ │ │ │ │ ├─────────┘ │ │ │ │ │ ├─────────┘ │ │ │ │ └───┤ │ │ │ │ ├───────────────────────────┘ │ │ ├───────┘ │ └─┤ │ └───────────────────────────────────────────┘ which normalizes to an infinite list of booleans. This can also be concisely converted [4] into a list of primes written in decimal. [1] https://tromp.github.io/cl/cl.html https://tromp.github.io/cl/cl.html [2] https://tromp.github.io/cl/Binary_lambda_calculus.html#Complexity_of_Sets https://tromp.github.io/cl/Binary_lambda_calculus.html#Compl... [3] https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html [4] https://www.ioccc.org/2012/tromp/hint.html https://www.ioccc.org/2012/tromp/hint.html
- Suskewiet 4y ago
  John, Thanks for the feedback. Really taking it to the limit. Very interesting reads. Bumped into them while doing this exercise, but did not dive in (yet).

15 points by Suskewiet 4y ago

Suskewiet 4y ago

Writing a prime number generator in lambda calculus, starting from first principles.

martyalain 4y ago
Hi Suskeviet, So many way to play inside the good old holy world of lambda-calculus! The following document: http://jwodder.freeshell.org/lambda.html 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=lambdacalc http://lambdaway.free.fr/lambdawalks/?view=lambda_calculus http://lambdaway.free.fr/lambdawalks/?view=lambda_calculus http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=fromroots2canopy http://lambdaway.free.fr/lambdawalks/?view=coding 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/ http://lambdaway.free.fr/lambdawalks/ I would be interested in your opinion.
- l- 4y ago
  Regarding http://jwodder.freeshell.org/lambda.html http://jwodder.freeshell.org/lambda.html, "B" is Hypothetical Syllogism (transitivity of implication (the "material conditional")), which is the composition of the arguments x and y applied to the argument z (https://en.wikipedia.org/wiki/B,_C,_K,_W_system https://en.wikipedia.org/wiki/B,_C,_K,_W_system) rather than the composition of the arguments x and y alone. > 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.htm 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-questions-page.htm https://web.ics.purdue.edu/~dulrich/Twenty-six-open-question...) would seem to mean λx. x B K is as short as possible.
  - tempodox 4y ago
    > "B" is Hypothetical Syllogism Is it so hypothetical? I'd have thought that function composition fits the Barbara syllogism.
    - l- 4y ago
      Barbara & the other (categorical) https://en.wikipedia.org/wiki/Syllogism https://en.wikipedia.org/wiki/Syllogism take the "existential viewpoint" (see introduction on https://en.wikipedia.org/wiki/Categorical_proposition https://en.wikipedia.org/wiki/Categorical_proposition) that involves "term": https://en.wikipedia.org/wiki/Term_logic https://en.wikipedia.org/wiki/Term_logic instead of just "sentential": https://en.wikipedia.org/wiki/Propositional_calculus https://en.wikipedia.org/wiki/Propositional_calculus logic. From https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... the universal quantification "all" in Barbara corresponds to the generalized product (conjunction rather than implication) type. B is also known as the composition combinator & (implicational) forms are shown here: https://en.wikipedia.org/wiki/Hypothetical_syllogism#Alternative_forms https://en.wikipedia.org/wiki/Hypothetical_syllogism#Alterna...
- Suskewiet 4y ago
  Alain, 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.

tromp 4y ago

A much more concise prime number generator in lambda calculus [1] [2] is λ (λ 1 (1 ((λ 1 1) (λ λ λ 1 (λ λ 1) ((λ 4 4 1 ((λ 1 1) (λ 2 (1 1)))) (λ λ λ λ 1 3 (2 (6 4))))) (λ λ λ 4 (1 3))))) (λ λ 1 (λ λ 2) 2) or in graphical notation [3] ───────────────────────────────────────────────── ┬─┬───────────────────────────────────┬──── ────┬ │ │ ┬─┬ ────┬─┬────────────────────── ┼───┬ ┬───┼ │ │ └─┤ ────┼─┼───────────────────┬── ┼───┼ │ ┬ │ │ │ │ ┬───┼─┼───────────────────┼── ┼─┬─┼ │ ┼ │ │ │ │ │ ─ ┼─┼─┬─────┬──── ──────┼─┬ │ ├─┘ └─┤ │ │ │ │ │ ┬ └─┤ │ ┬─┬ ┼─┬─┬ ──┬───┼─┼ ├─┘ ├─┘ │ │ │ └─┤ └─┤ └─┤ │ ├─┘ ──┼─┬─┼─┼ │ │ │ │ │ │ │ │ ├─┘ ┬─┼─┼─┼─┼ │ │ │ │ │ │ │ ├─┘ └─┤ │ ├─┘ │ │ │ │ │ │ └───┤ │ ├─┘ │ │ │ │ │ │ │ ├─┘ │ │ │ │ │ │ ├─────────┘ │ │ │ │ │ ├─────────┘ │ │ │ │ └───┤ │ │ │ │ ├───────────────────────────┘ │ │ ├───────┘ │ └─┤ │ └───────────────────────────────────────────┘ which normalizes to an infinite list of booleans. This can also be concisely converted [4] into a list of primes written in decimal. [1] https://tromp.github.io/cl/cl.html https://tromp.github.io/cl/cl.html [2] https://tromp.github.io/cl/Binary_lambda_calculus.html#Complexity_of_Sets https://tromp.github.io/cl/Binary_lambda_calculus.html#Compl... [3] https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html [4] https://www.ioccc.org/2012/tromp/hint.html https://www.ioccc.org/2012/tromp/hint.html

Suskewiet 4y ago
John, Thanks for the feedback. Really taking it to the limit. Very interesting reads. Bumped into them while doing this exercise, but did not dive in (yet).