algorithmic information theory

Stream: new members

[Rudi Cilibrasi]

greetings my new Friends! i like graph theory and automated theorem proving, looking forward to learning lean. Previously made a first order predicate logic theorem prover using linear resolution with paramodulation in the 1990's. Trying to understand lean better since last week i learned that the main theoretical math I help create twenty years ago was finally used in a proof using lean in "A parametrized family of Tversky metrics connecting the Jaccard distance to an analogue of the normalized information distance"

[Eric Rodriguez]

Paramodulation! We were having an interesting time with that a while ago trying to figure out the proof of things like McCune's axiom. Welcome, you may want to check out [stream#graph theory]

[Rudi Cilibrasi]

thank you @Eric Rodriguez i am in the stream and appreciate the pointer!

[Alex J. Best]

There has also been some discussion / PRs about Jaccard distance here before, hopefully you can find it by searching (I'm on mobile so unfortunately can't right now)

[Arthur Paulino]

Hey @Rudi Cilibrasi I am new to lean and I like graph theory too. If you'd want to team up, I'm a bit stuck on this branch. We're trying to formalize graph coloring as an homomorphism to a complete graph. You can check src/combinatorics/simple_graph/coloring.lean

[Rudi Cilibrasi]

thank you Arthur! that would be awesome if i can reach that level but first i will need to do the basic tutorial and environment install. thank you for this invitation it seems like a perfect introduction unless i discover it's really too hard in which case i am still happy for the practice learning

[Kevin Buzzard]

Several people have learnt a working knowledge of Lean by working on graph theory -- I think it's quite a nice entry point.

[Bjørn Kjos-Hanssen]

Hi @Rudi Cilibrasi ! That's my paper - https://arxiv.org/abs/2111.02498 (notice the "Code &Data" link) I got a lot of help from people here on the Lean part, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Jaccard.20distance The paper is about an analogue of the NID (normalized information distance). Formalizing the NID itself would require first formalizing Kolmogorov complexity which I don't think has been done(?).

[Rudi Cilibrasi]

Wow thanks for this great detail Bjorn!

[Rudi Cilibrasi]

Have we got a Turing machine in math lib yet by any chance?

[Bjørn Kjos-Hanssen]

https://leanprover-community.github.io/mathlib_docs/computability/turing_machine.html

[Bjørn Kjos-Hanssen]

I don't see anything about existence of a universal Turing machine there, though?

[Mario Carneiro]

There is a universal partial recursive function, and some work on connecting turing machines to the partial recursive functions that is mostly complete but not all the library lemmas are there

[Mario Carneiro]

See https://leanprover-community.github.io/mathlib_docs/computability/halting.html for stuff about universal machines

[Bjørn Kjos-Hanssen]

@Mario Carneiro great, the universal partial recursive function could be used to define Kolmogorov complexity I suppose

[Mario Carneiro]

yes, I think that would work fine

[Mario Carneiro]

There is the docs#nat.partrec.code type for expressing partial recursive functions as elements of a countable type

[Rudi Cilibrasi]

is a countable type like peano integers?

[Mario Carneiro]

more precisely, docs#denumerable

[Rudi Cilibrasi]

i see zero and succ which seem familiar to me from that in that code

[Mario Carneiro]

yes, nat is the canonical denumerable type

[Mario Carneiro]

a denumerable type is one that is isomorphic to nat

[Rudi Cilibrasi]

great makes total sense

[Mario Carneiro]

in particular, this matters for encoding because the isomorphism gives you a way to assign bit sequences or so to individual programs

[Mario Carneiro]

so you can ask what is the 5th program

[Mario Carneiro]

and more complicated programs get bigger numbers

[Rudi Cilibrasi]

yes that seems pretty close to what would be required to define K and C kolmogorov complexity

[Arthur Paulino]

Btw I was reading turing_machine.lean today (haven't finished it yet) and it inspired me :pray:

[Mario Carneiro]

incidentally, the 5th program is prec zero zero which is another way of writing the zero function:

import computability.halting

open nat.partrec (code)
attribute [derive has_reflect] code
#eval let r := denumerable.of_nat code 5 in pp (reflect r) -- prec zero zero

#eval ((denumerable.of_nat code 5).eval 42).get undefined -- f 42 = 0

[Reid Barton]

What about the 37th program

[Reid Barton]

that seems more useful

[Mario Carneiro]

that's prec left left apparently, which is 0 for 0 and (nat.unpair (n-1)).1 otherwise

[Rudi Cilibrasi]

wow these are great programs!

[Rudi Cilibrasi]

i shouldn't let my imagine wander too far but i wonder how big the program must be to be turing complete

[Rudi Cilibrasi]

my friend john tromp is super into that question and has enjoyed writing up some pretty small turing machines on the order of dozens of bytes
... the rules aren't totally clear to that game though in the literature imo. which is why finding an answer with lean would be super interesting.

[Mario Carneiro]

I really enjoyed watching the discussion around Aaronson & Yedidia's search for the smallest unprovably halting TM, which resulted in an optimizing compiler for turing machines

[Mario Carneiro]

In principle, you should be able to extract the proof of computability in docs#nat.partrec.code.eval_part and turn the witness into a number, but I have reasons to believe that the result is very large and lean will probably not be able to handle it

[Kyle Miller]

While it's not a Turing machine, the binary lambda calculus is kind of neat. There's a 206 bit self-interpreter at https://tromp.github.io/cl/cl.html (more details: https://tromp.github.io/cl/Binary_lambda_calculus.html)

[Rudi Cilibrasi]

i installed lean just now and the vscode extension to try to reproduce Mario first example above for program 5. i cannot import computability.halting should i use elan to fix it or what?

[Rudi Cilibrasi]

yup thats my john too kyle he is super into it

[Mario Carneiro]

You need mathlib as well. See https://leanprover-community.github.io/get_started.html

[Kyle Miller]

Rudi Cilibrasi said:

yup thats my john too kyle he is super into it

(Oh, I completely missed that you said his last name earlier!)

[Rudi Cilibrasi]

how do i install computability.halting i am having trouble with the command
i think i have mathlib in there but i guess i can't be sure

[Rudi Cilibrasi]

i tried on two different linux

[Rudi Cilibrasi]

Otherwise pipx is ready to go! :sparkles: :glowing_star: :sparkles:
installed package mathlibtools 1.1.0, Python 3.8.10
These apps are now globally available

- leanproject

done! :sparkles: :glowing_star: :sparkles:
rudi@rsys:~$ cd ~/tmp

[Rudi Cilibrasi]

oh maybe pipx?

[Rudi Cilibrasi]

probably i will have to run a tutorial to figure out this new package management tool and determine if i really have mathlib or not. at least the eval 1+1 part did appear to work so something is working

[Alex J. Best]

Are you following the instructions at https://leanprover-community.github.io/install/debian.html ? And then on the linked at the bottom for lean projects?

[Alex J. Best]

Or https://leanprover-community.github.io/install/linux.html if not debian/ubntu?

[Rudi Cilibrasi]

yes i did follow that page... the wget way twice and also went through the long step way a bit too.. i am on 20.04 ubu
but i did not do lean projects at the bottom yet i guess that could be my problem

[Rudi Cilibrasi]

oh i see now i must need a project to add deps. cool! ty Alex

[Alex J. Best]

Yes mathlibtools is a helpful python package, it won't download any actual mathlib olean files for you to import things unless you give it a reason to, either you are working on your own local fork of mathlib, or a project that depends on it.

[Rudi Cilibrasi]

it works now i verified mario's first result. ty for help friends i have tried lean a few times before in earlier years and version 2 but i never got far and now in only one afternoon i feel like i am already equipped to make independent slow progress.

[Rudi Cilibrasi]

i am able to read and understand the succ and zero definitions in nat.partrec.code quite easily but the id, pair, left, and right are confusing me. i feel like i am not getting it. i am familiar with tuples, cartesian pairs, currying and element-extraction functions in other languages and high school math. i reviewed the equations definition in partrec_code.html for these and still feel like i must be missing some code. i'm familiar with how to draw a spiral in cartesian integers to show equivalence of the lattice to the line and back but i don't quite see it here yet. just another newbie question when somebody has time. meanwhile i will start to work more tutorial

[Mario Carneiro]

Note that nat.partrec.code doesn't explain what the functions actually do, it is only the raw structure of the program. A better place to look to understand what all the constructors do is docs#nat.partrec, which has the exact same constructors but it is talking about actual nat ->. nat partial functions

[Mario Carneiro]

In particular, to understand what left and right are doing you should look at docs#nat.unpair - the short answer is that it is the inverse to the cantor pairing function (or rather a slight variant on the cantor pairing function)

[Mario Carneiro]

We use these functions so that we can pack multiple variables into a single nat, using pair to put nats together and left/right to pull out the pieces

[Rudi Cilibrasi]

ok i've invited some of my science friends paul and joseph and soon i think i will invite john
lean is so much cooler now with the zulipchat :)

[Rudi Cilibrasi]

i want to get this K or C kolmogorov complexity show on the road

[Rudi Cilibrasi]

usually i think the most important weird math function necessary when talking about K and C is log. I see there is a nat/log in mathlib would that be appropriate to use for proofs bounding K and C?

[Bjørn Kjos-Hanssen]

Looks like nat.clog would be more useful when the log is in the upper bound

[Bjørn Kjos-Hanssen]

And nat.log when it's in a lower bound of K or C

[Rudi Cilibrasi]

excellent hint ty Bjorn!

[Rudi Cilibrasi]

Hmm I think maybe our aforementioned @John Tromp could be awake …

[John Tromp]

hi, Rudi

[John Tromp]

and lean fans

[Rudi Cilibrasi]

We have been talking about formalizing K and C in here as shown above largely based on Mario work already done with partial recursive universal fn

[John Tromp]

i don't know much about lean, but happy to answer any questions about binary lambda calculus

[Rudi Cilibrasi]

We also noticed lean mathlib already has nat log and clog suitable for basic theorems about K and C

[John Tromp]

i guess lean can prove any reduction in the untyped lambda calculus?

[Rudi Cilibrasi]

Oh I would assume so. It was @Kyle Miller who mentioned the binary lambda calc

[Mario Carneiro]

what is K and C? Does that stand for something?

[Mario Carneiro]

Lambda calculus is not defined in mathlib, but it could be

[John Tromp]

i use KS and KP in my paper instead of C and K

[Mario Carneiro]

are these combinators?

[John Tromp]

KS/C is plain complexity, with delimited programs

[Mario Carneiro]

oh, that

[John Tromp]

KP is prefix complexity, with self-delimited programs

[Mario Carneiro]

How precisely do you want to get the kolmogorov complexity definition? As I understand it you can get within a constant additive factor without trouble but the exact definition is language dependent

[Mario Carneiro]

so that would mean formalizing e.g. binary lambda calculus

[Mario Carneiro]

rather than anything with equivalent computational strength

[John Tromp]

yes, for theorem proving you want precise definitions. such as the TMs counted in https://oeis.org/A141475

[John Tromp]

or the KP/KS in my paper

[Kyle Miller]

@John Tromp There's a variation on binary lambda calculus that I've played with a little, but I haven't tried making a competitive self-interpreter with it yet (and I don't really expect it to be able to make terser programs). The idea is you let the De Bruijn indexing's successor (that's usually only for indices) apply to entire expressions. The interpretation is that everything inside the successor of an expression forgets the current innermost binding. This lets you factor out taking successors in applications if both variables in the application are nonzero indices.

inductive lambda
| get : lambda
| drop : lambda → lambda
| app : lambda → lambda → lambda
| abs : lambda → lambda

For the binary encoding, it's still a prefix code, but the codes are now just all four two-bit sequences.

[John Tromp]

so drop E is E with all de bruijin indices of free variables increased by 1?

[John Tromp]

and then get is equivalent to var 0

[John Tromp]

interesting variation!

[Kyle Miller]

Yep, or if you're thinking about it in terms of an evaluator that has a list of values for each de Bruijn binding, drop drops the first entry of the list, and get gets the first entry.

[John Tromp]

for instance S = \ \ \ 2 0 (1 0) becomes \ \ \ (+ + 0) 0 ((+ 0) 0)

[John Tromp]

in which case you get no savings, and get a longer program

[John Tromp]

hard to say if the interpreter would get longer or shorter though. without actually writing it out

[John Tromp]

i'll try it out tomorrow. close to bedtime now:)

[John Tromp]

the interpreter itself becomes simpler, but its encoding becomes larger: 222 instead of 206 bits

[John Tromp]

so for the goal of minimizing program sizes, i should stick with the current variable encoding

[John Tromp]

btw, there is only one occurrence in the interpreter where a drop can apply to an expression larger than one variable

[Kyle Miller]

Interesting -- thanks for looking into it. The reason I'd thought of it in the first place was to simplify case dispatch in the main loop, since there's now only a single inductive type rather than two.

Do you think it could be improved by using a base-4 stream with the encoding $\lambda\lambda\lambda\lambda i$ for $i=0,1,2,3$? (Each of these would still count as two bits of course.)

[Rudi Cilibrasi]

Hey is @Joseph Dimos here yet?

[Joseph Dimos]

Greetings everyone! I like argumentation theory and its alignment with ATP. I often venture into applied category theory problems that interlace with satisfiability problems. Previously, I defined a formal chaining inside linear temporal logic and defined a dualistic theme for doxastic and epistemic logics according to belief probability. I'm also involved in some quantum gravity related problems that interlace 6j symbols with fusion categories in gauge theory. I'm quite interested in Lean, but am still learning its many facets.

[Rudi Cilibrasi]

Glad to see you here Joseph!

[John Tromp]

no, the interpreter makes very good use of the 2-bit encoding. moving to base 4 would certainly expand it significantly

[Yaël Dillies]

Rudi Cilibrasi said:

Glad to see you here Joseph!

Wow, you can wish people in existence!

[John Tromp]

Btw, there's a language called "Real Fast Nora's Hair Salon 3: Shear Disaster Download" (yes, really!) that looks similar to your proposal, Kyle.

[John Tromp]

https://esolangs.org/wiki/Real_Fast_Nora%27s_Hair_Salon_3:_Shear_Disaster_Download

[John Tromp]

Except they forgot to generalize to applying the ONE MORE THAN operator to arbitrary terms (while changing its encoding to 11).

[Eric Rodriguez]

Wow, the guy who made that is called Nathan van Doorn, but they are not related to Floris

It strikes me as a very weird coincidence that there's someone out there doing the kind of research that I'd very much like to be doing, with the same fairly uncommon surname as me, who is not to my knowledge related to me (if you read this, hi Floris)

- Nathan van Doorn (@Ngevd)

[Kevin Buzzard]

@Floris van Doorn just to check you see this!

[Floris van Doorn]

Haha, that's great. I've contacted him.

[Floris van Doorn]

Thanks for the ping.

[Kyle Miller]

@John Tromp I guess my variant must be "Real Fast Nora's Hair Salon 4: A Little off the Top"