Boole theorems

Stream: CSLib

[Arthur Paulino]

Pasting a question I asked which couldn't be answered due to time constraints:

Since the algorithms will be represented as Lean data (terms of a Boole type?) and not Lean definitions, how will theorems be proven? Will Boole have to reimplement the mechanics that Lean has in order to introspect on the body of functions to prove its own theorems (not Lean theorems)?

[Eric Wieser]

My understanding (without any context beyond the slides and discussion) is that we would end up with something like def mergeSort : Boole (List α → List α), and then the theorem about correctness would be something about mergeSort.eval l : List α

[Ayhon]

Why Boole (List a - > List a) over List a - > Boole (List a) ?

[Ayhon]

I know this is all still hypothetical, but thats what I thought about first

[Alex Meiburg]

Ayhon, the latter option you wrote would mean "a Lean function which takes a List, and gives you a Boole function genList() with no arguments which produces a list".

In terms of reasoning about correctness (it produces a sorted permutation) that would work, but it omits everything about computation time or memory: the "outer" Lean function could rely on anything, be exponential time, or even on undecidable statements - and spit out an O(1) "sorting algorithm" that returns an appropriate constant.

By wrapping the whole thing in Boole, you start to talk about the whole process.

[Ayhon]

Hmm, so then Boole in this context is literally the semantic function, which translates the algorithm to a List a - > List a? Or more so, the Boole.eval is that function

[Ayhon]

This feels like denotational semanrics, I think?

[Clark Barrett]

I believe the answers to these questions will become clearer once we have the initial release of Amazon's MIDI language framework - goal is end of this month.