How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

Question

Question:

Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms.

I'm wondering whether Lean4 (or a typical well-known PA) just stores new kinds of operation expressions as strings, lists, expression trees or...? Could you link me to the specific part in the Lean4 code that defines these classes or structs?

I'm fairly certain that it doesn't implement a new class in its kernel for each operator, because it supports almost any Unicode string as an operator symbol (?)

So what data structure does lean use internally to represent the expressions that are the definition part of its lambda functions. I'm assuming it's based upon Lambda functions, because it's Type Theory-based, and usually or so I thought each of those systems appeals to these types expressions.

I am not sure whether I'll support every operator under the sun, but I at least want every operator appearing in Algebra by Serge Lang, for example. Well, they don't mention wreath product in that book, so in essence, your typical math book plus a few exotic operators. But it should be straight-forward to add in new operators, i.e. not a week-or-more of debugging to get them to work.

You can stop reading here, the below is just extra information

---

I'm not going to represent things as Unicode as Lean4 does, instead I'm going the LaTeX approach. Everything the user types in, there is a live preview that renders LaTeX / Markdown. If anyone is interested, the canonical example of such an editor (with no PA or any kind of math backend) is:

Marked / KaTeX rendering from within a Qt/C++ app

I did not come up with that on my own. It's an example provided by Qt, the markdown portion. I did add in support for KaTeX, but it was easy. If you'd like say to add in support for the Quiver editor on the JS side, you'd have to figure out how the QWebChannel communication code works.

My Background:

I know a lot of math (check out my MSE profile). I have been coding for over 10 years. I know the essentials to get a DSL or programming language up and running, but have never actually finished & publically shared one. The D language has this nice parser generator called pegged, which allows you to specify PEG grammars. I am intermediate at it. It's a lot more user friendly to me than ANTLR or bison / lex. I by no means want to compete with Lean4 or anything. My goal is to do diagram chase-based proofs, but of course I need to support at least polynomials, and then a can of worms is opened into the world of PA's. I have coded many frontends for diagram editors, but always seem to get stuck on the logical backend or the PA-related system. A book recommendation would be nice. I think I want to stick with natural deduction and set theory axioms, and not delve into Type Theory quite yet. I would like the presentation of my system to be as close of a match to mathematics as-you-see-it in rigorous, formal-yet-human-readable textbooks.

So what I lack is "formalized logic theory" knowledge, Compiler Design, Type Theory knowledge. I figured I am good enough of a programmer to tackle what I need to, though, without taking graduate-level courses to understand some of this stuff. I figure, if I know math and I know how to program, then I should be able to come up with something. Just something that would be of value to mathematical users.

Answer 1

(This answer assumes you already know some of the basics of Lean as in Theorem Proving in Lean 4.)

In a typical first logic class or set theory class in college, first order logic is presented as taking place in a particular language (or signature). ZFC for example is in the language with only one binary relation $\in$. (The basic logic operations and quantifiers are also assumed usually, including $\exists$, $\forall$, $\rightarrow$, $\land$, $\lor$, $\neg$ and $\leftrightarrow$ as well as parenthesis and variables). All other definitions are just abbreviations for a longer expression. However, in practical proof assistants this isn't practical. We must have the ability to make definitions (and theorems, axioms, etc) first class citizens.

The way Lean (and I assume Coq and Agda) do this is to store declarations. In Lean the type Declaration can be any of the following:

• axioms
• definitions
• theorems
• ...

A Definition is made up of the following parts:

• the name of the definition
• the type of the definition
• the value of the definition (i.e. the body of the definition after the := in Lean)

...as well as some more technical details. Theorems are similar, except the type is the statement of the theorem and the value is the proof. (In dependent type theory, unlike other logics, definitions and theorems are mostly the same thing, with the differences being mostly technical details in how each is implemented and stored.)

Going down the rabbit hole, the type and value of a definition or theorem is an expression Expr. Before going into Lean expressions, let's recall expressions in a simpler logic like propositional logic. In propositional logic, a well-formed-formula (wff) is defined (inductively) to be any of the following forms:

• a propositional variable $P$
• a negation $(\neg \phi)$, for an wff $\phi$
• $(\phi \square \psi)$ for $\square$ in $\rightarrow$, $\land$, $\lor$, $\neg$ and $\leftrightarrow$ and wffs $\phi$ and $\psi$.

The idea of a Lean expression is similar, except that it doesn't make sense to hard code the logical symbols like \land. Ignoring notation and unicode characters in Lean, the way that Lean would represent and P Q would first use Currying to represent it as (and P) Q and then use an applicative operator to represent that as app (app and P) Q. The applicative operator app fn arg means apply the function fn to the argument arg. The major exception to this in Lean is -> (both the logical implication and the function arrow as in Nat -> Nat since they are the same thing). A -> B is just an abbreviation for forall (_ : A), B or Pi (_ : A), B.

Now for more of the specifics. An Expr can be any of the following:

• a bound variable bvar n, where n is a number (the DeBruijn index) saying how many levels one has to go up to get to the corresponding quantifier. This has many advantages over storing the variable name directly.
• a free variable fvar nm where nm is a unique name for that free variable.
• a sort sort lvl where lvl is the level of that sort, e.g. Prop is level zero, Type is level one, Type u has level u+1 where u is a universe variable)
• a constant const nm where nm is the name of some definition, theorem, axiom, etc already in the library.
• an applicative app fn arg where fn is the expression for the function and arg is the expression for the argument of the function.
• a lambda expression lam nm tp body bi where nm is the name of the variable for that lambda binder, tp is the expression for the type of that variable, body is an expression for the body of the lambda (which might use that variable), and bi is some technical information about what kind of binder it is.
• a forall/Pi expression forallE nm tp body bi where nm, tp, body, and bi are just like in lambda expressions.

...as well as a few more less-used expression types.

---

There are many more implementation details to Lean. For example, type classes and notation are what let you use infix operators like + or list notation like [1, 2, 3] (as well as representing numbers as digits).

Turning human code into Lean expressions is a process known as elaboration. (Actually, I'm not positive on the differences between parsing, elaboration, and type checking. Although I do know that type checking is what checks that an expression is valid, and is also what checks that a proof is valid in Lean.)

Conversely, if you have an expression inside Lean, like the goal of a state in a tactic proof, the pretty-printer is what prints that expression in a form which is human readable Lean code.

The Lean 3 meta framework (similar to Lean 4's I believe) is described in the paper A Metaprogramming Framework for Formal Verification.

---

Ok, how would you implement all of the above? If you know functional programming, e.g. Scala, Haskell, OCaml, or even Lean 4 (which is a fully featured functional programming language itself used to implement Lean), then this should appear familiar to you. Declarations, expressions, universe levels, etc are all just implemented as inductive data types (or what some functional languages call algebraic data types). A good exercise is to code up in your favorite functional programming language the data types of well-formed formulas in propositional logic as I described above.

If you aren't working in a functional language, but instead in a low level language like C, then I think you would have to consult the best practices for your language, and just look up "how do I implement algebraic data structures in X language". However, Lean 4 is implemented in C++ as well. (Specifically, C++ is used to boot-strap Lean 4 so you can build Lean 4 in Lean 4.) I think expressions are implemented in the file expr.h.

---

This is only scratching the surface, but hopefully it gives you a flavor and some references and keywords to explore on your own.