AI Assisted Proofs

Compared to model checkers that just exhaustively search a well-defined state space, there's not a lot of reason to believe in opaque, large proofs of interactive theorem provers at this moment. Four reasons. 

1. There's a problem with the math. If there's one 'paradox' like Banach-Tarski, there are probably an infinite number of them. What if the proof exploits one?
2. There's a problem with the logic. At one point in time, I understood the rather simple type theories people worked with. I don't understand the current ones, so maybe I shouldn't comment on it, but I am unsure how robust they are. 
3. There's a problem with the implementation of the type theory. Usually, that would boil down to a kernel bug, but there's ample reason to believe it may lie elsewhere. For example, the presentation of a proof.
4. There's a problem with the formalisation. I.e., something was stated, but it turns out that didn't reflect the math correctly, and subsequently something else was proven.

I don't really trust these latest proofs, but at the same time, I am not that sceptical. I would call it a coin flip.

Peirce's Law in Egel

 Like Scheme, Egel has a trivial inhabitant of Peirce's Law ((p->q)->p)->p too.

def peirce = [F -> try F [X -> throw X] catch [X -> X]]

The combinator peirce has Peirce's law as type and takes as an argument a function F of type (p->q)->p and we feed that function another function of type p->q that throws its argument X of type p to the outer scope.

Utter bullshit, of course. 

Matching recurring variables

The Egel interpreter is about a decade old, and I thought I kinda milked it already for all the blog posts I wanted to write about it. 

 The best overall feelings I have about the interpreter can be summed up as: A) It's a fine toy esoteric language, but please don't use it professionally. And B), I have a lot of fun coding Advent of Code solutions in it, and there's something to the language, but I cannot quite pinpoint what. 

Someone asked me where Egel would fall compared to other languages, and I am not entirely sure about that either. Q/Pure, Maude, Wolfram Language or something defined in Racket might be close. 

Refal came up during that discussion, and I looked into it. One thing that struck me is that Refal can pattern-match recurring variables. I could extend Egel with that, maybe. That would allow definitions like `def eq = \x x -> true | _ _ -> false`. It seems non-trivial, but on the other hand, all the machinery should be in place. But at the same time, it doesn't seem to useful a feature.

Lazy Streams

 I did a small Lean experiment with lazy streams.  It failed, but I wanted to write it down anyway.

inductive Sequence (α : Type u) : Type u

| nil : Sequence α

| cons : α → (Unit → Sequence α) → Sequence α

Let's look at slices

def slice : Nat → Sequence α → List α

| 0, _ => []

| _, .nil => []

| n + 1, .cons a f => a :: slice n (f ())

and prove the following.

theorem sequence_extensionality {α : Type u} (s₁ s₂ : Sequence α) :

 (∀ n : Nat, slice n s₁ = slice n s₂) → s₁ = s₂ := by

    sorry

So far so good. But unfortunately, this models finite lists. On the following, Lean cannot prove termination.

def zeroes : Sequence Nat := Sequence.cons 0 (fun x => zeroes)

Moreover, falsum is trivially inhabited by induction. 

example (x : Sequence Nat) (h : x = .cons 0 (fun _ => x)) : False := by

induction x with

 | nil =>

contradiction

 | cons a f ih =>

     simp only [Sequence.cons.injEq] at h

     apply ih ()

     conv => lhs; rw [h.2]

     dsimp

     rw [h.1]

We could try the following, but it just results in finite lists.

def zeroes : Nat -> Sequence Nat

| 0 => .nil

| n + 1 => .cons 0 (fun _ => zeroes n)

End of experiment for me, I was just interested whether a formalization like this could work.

Lessons learned from Advent of Code 2024

 I should have kept a log, but here we are: a bullet list of lessons learned from Advent of Code this year in no particular order.

• Egel is a fine language for short scripts, but—here we go again—it lacks an order in performance.
  
• When I do stuff right, and this year I did, Egel programs are comparable in size to Haskell programs but -in my mind- way more readable.
  Where Haskell shines is sometimes clever use of laziness and -very important- list comprehensions. Egel sometimes shines because of clever use of dynamic typing (usually the use of none), and having mutation.
  In comparison to K, both Haskell and Egel take an order more symbols. Ken Iverson was on to something.
• Where Egel is slow that is usually due to several factors.
  
  First, the interpreter implements a slow rewriter and something like a one-instruction increment which comes at virtually no cost in most imperative languages takes orders, and not a small amount, more.
  
  Then second, I often iterate over dictionaries, which means first creating the list of keys and then folding over all those keys. I am not sure that is even that hefty a cost, but I should probably write folds and maps for dictionaries.
  
  Third, looking up a value in a dictionary costs much more than indexing in an array.
  
  That means that one example, day 6, which involves an enormous amount of iteration over a board, is very, very slow and times in at 12 minutes.
•  I added namespace mechanisms and that seems to be a win. Because I added namespaces however, and I still wanted to be able to include the out-of-the box utilities with a short statement I decided to uniquely name all combinators. (I.e., you'll normally find a length operator on lists, strings, and dictionaries, those now all have different names.)
  That was a mistake, roughly I need to use the namespaces where nothing in System, OS, and List overlaps but it's fine to have a length operator on strings and use the namespace mechanisms to rename or include that in the manner deemed fit.
  
• I should implement more generic combinators akin to Python or array languages like J/K. Just having add on atoms and complex data shortened the code substantially.
• I still get bitten by `-1` versus `-` `1`. I also got bitten by my dumb operator precedence heuristic, the latter did fine for a while but now I need to fix that.
  
• At the end of Advent of Code, programs become longer, and development becomes painful in Egel. I expected this but Egel is indeed only usable for relatively straightforward code.
  For short programs, something like a missing or wrongly named argument is trivially found by inspecting the output after running the program. For longer complex programs, it becomes hard to see where the bug is without strong typing.
  
• There was a segfault somewhere during coding this month I can no longer reproduce.

Egel is, after several years of ad-hoc development, still in an alpha stage. But I am getting there.

Egel programs and several metrics are in the README.

Namespaces, revisited.

I conservatively extended namespaces, but that took an internal overhaul of how scopes are treated. Shorthands are syntactic sugar for full-blown expressions.

using System

The above is sugar for:

using System (c0, c1, c2, ...)

Where c0, c1, c2, ... are all combinators in the System workspace. And that is sugar for:

using ε = System (c0, c1, c2, ...)

Which is again sugar for a number of renames.

using ε = System (c0 = c0, c1 = c1, c2 = c2, ...)

The renames all introduce bound names into the current scope. E.g.,

using Sys = System (p = print)

This will bind 'Sys::p' to 'System::print'.

Docstrings

I added docstrings to the Egel language some time ago. You can add documentation to either a file or a combinator.

@"""A multiline docstring for a file"""

def f =
    @"this is the fabulous 'f' combinator"
    [X -> 42]

Given docstrings, you can now ask for that interactively in the REPL.

>> help 'f'
{"this is the fabulous 'f' combinator"}

'Help' will do a best-match against all combinator definitions.