Binary Lambda Calculus (2020)(tromp.github.io)

tromp.github.io

Binary Lambda Calculus (2020)

https://tromp.github.io/cl/Binary_lambda_calculus.html

16 comments

Ameo4 anni fa

> Roughly speaking, the complexity of an object is the length of its shortest description.

This has a ton of really interesting implications.

Even though Kolmogorov complexity is technically incomputable due to the halting problem, you can estimate it. One method of doing that is to create a bunch of random Turing machines and see how often they produce some output string[1]. You have to cut them off after running for a while to prevent infinite loops but it turns out that the output probability of a string strongly correlates with its Kolmogorov complexity.

This works for neural networks as well. You can treat a neural network as a binary classifier, or more generally a boolean function that has some number of binarized inputs mapping to a single binary output.

I explored this a bit in a blog post I wrote a while ago[2]. By randomly initializing weights and counting the truth tables produced, you can estimate Boolean complexity for different expressions which is NP hard.

[1] https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4014489/

[2] https://cprimozic.net/blog/boolean-logic-with-neural-network...

[deleted]4 anni fa

codeflo4 anni fa

What the paper you linked to is doing is an interesting statistical analysis of the behavior of random Turing machines for a given time limit.

I just don’t agree that this can be fairly summarized as “estimating Kolmogorov complexity”.

Kolmogorov complexity isn’t a statistical measure — it doesn’t matter how unlikely the machine that produces the output string is. And the time limit they have to impose to actually run those machines is crucial; some of the machines they have to abort would eventually produce an output and halt.

tromp4 anni fa

A BLC interpreter [1] won in the 2012 International Obfuscated C Code contest [2].

BLC provides a functional busy beaver function [3] that is more fine-grained than the TM-based one.

The byte oriented version BLC8 is one of the 128 languages in the quine relay [3].

[1] https://www.ioccc.org/2012/tromp/tromp.c

[2] https://www.ioccc.org/2012/tromp/hint.html

[3] https://oeis.org/A333479

[4] https://esoteric.codes/blog/the-128-language-quine-relay

zaik4 anni fa

A program in Binary Lambda Calculus to compute the Ackermann function is less than 7 bytes: https://codegolf.stackexchange.com/a/83924

akomtu4 anni fa

I struggled to understand what the author is talking about, and the wikipedia page about lambda calculus only added confusion, but I feel like I sensed the idea behind it: "by skillfully combining a few basic functions, we can produce any output we like, and by skillfully encoding those skillfully combined functions we can compress any data into a particularly compact program." Is this a good summary?

sabalaba4 anni fa

I re-implemented this in python. Was a pretty fun project. Tromp is awesome.

http://stephenbalaban.com/a-binary-lambda-calculus-parser-in...

dang4 anni fa

Related:

Binary Lambda Calculus (2012) - https://news.ycombinator.com/item?id=26769650 - April 2021 (12 comments)

Most functional (tromp - implementing Binary Lambda Calculus) - https://news.ycombinator.com/item?id=4673056 - Oct 2012 (1 comment)

Others?

73737373734 anni fa

Related: Iota, Jot and Zot by Chris Barker:

https://en.wikipedia.org/wiki/Iota_and_Jot

http://cleare.st/code/iota-jot-zot

> Every combination of 0's and 1's is a syntactically valid Jot program, including the null program.

tromp4 anni fa

While these are very simple universal languages, as is a simple binary language based on S K combinators (see Section 3.2 of [1]), they don't yield the very compact programs that BLC does.

[1] https://tromp.github.io/cl/LC.pdf

potiuper4 anni fa

Iota appears to be the same as the "X" combinator as found by Jeroen Fokker: The Systematic Construction of a One-Combinator Basis (1989) that amounts to concatenating/applying (material) implication's reduction & distributivity axioms ("S" & "K") in addition to first binding another variable "x", which is "f" in the Iota definition. Shorter than "x" locally complete & consistent (indecisive) single implication axioms exist as one found by Meredith and listed by the now deceased Dolph Ulrich: https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page... See also: https://math.stackexchange.com/questions/153163/what-is-the-... The shortest single implication axiom appears to be an open question (though translating to implication the McCune/Fitelson/Wos/Wolfram shortest 6 NAND axiom work https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_alg... seems to be a proof for 3 variables) along with if distributivity is the shortest local completeness (weakening) axiom (see Robbins axiom & associativity & commutativity 3-basis) in addition to having to analyze Meredith's & others on Ulrich's list for self-interpreter lengths. But, a self-interpreter seems unlikely to be shorter compared to lambda calculus given the pattern of decreasing self-interpreter length with increasing complexity of the underlying axiom system.

[deleted]4 anni fa

nonrandomstring4 anni fa

Gives me an "Agent Smith moment", just marvelling at its beauty, it’s genius.

irsagent4 anni fa

I assume you can simulate a turning machine with it.

tromp4 anni fa

I don't know about turning machines, but it can certainly simulate Turing machines. You can even interpret Brainfuck, a Turing Machine inspired esoteric language, in under 104 bytes [1].

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Brain...

User234 anni fa

It’s a beautiful reification of de Bruijn indices. Thanks!

I’m kind of tempted by the idea of sugaring it using symbol properties such that one could use obfuscating names without breaking the elegant alpha compare and convert.