Comment by martyalain | Hacker News Reader

Comment by martyalain | Hacker News Reader

Parent Full thread

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 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.

Regarding 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) 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...

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.

> "B" is Hypothetical Syllogism

Is it so hypothetical? I'd have thought that function composition fits the Barbara syllogism.

Barbara & the other (categorical) https://en.wikipedia.org/wiki/Syllogism take the "existential viewpoint" (see introduction on https://en.wikipedia.org/wiki/Categorical_proposition) that involves "term": https://en.wikipedia.org/wiki/Term_logic instead of just "sentential": https://en.wikipedia.org/wiki/Propositional_calculus logic. From 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#Alterna...

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.

Reply on news.ycombinator.com