VM and axioms

Stream: new members

[Valery Isaev]

I saw somewhere a statement of the form "Lean has axioms, but they do not block computation because it is done in VM". I do not really understand this. You can use VM or compile code in machine instructions or interpret it. This is not related to axioms in any way. I think that there is a subset of the language that can be used in computation and you cannot use axioms in it, you can use axioms only in proofs which are never evaluated. This is all reasonable (assuming I'm correct), but this has nothing to do whether Lean computes the code in VM or in a different way.

[Matt Earnshaw]

it may be helpful to recall the precise statements from https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

on top of the underlying framework of universes, dependent function types, and inductive types, the standard library adds three additional components:

• the axiom of propositional extensionality
• a quotient construction, which implies function extensionality
• a choice principle, which produces data from an existential proposition.

The first two of these block normalization within Lean, but are compatible with bytecode evaluation, whereas the third is not amenable to computational interpretation. We will spell out the details more precisely below.

So firstly, we are only concerned with the effect of some specific axioms, not axioms in general. Then we are concerned with two notions of computation corresponding to lean's kernel and VM, respectively (witness also #reduce vs #eval). The former has a more "strict" kind of evaluation that uses the rules of type theory to reduce expressions, the latter is more "permissive" because it throws away type constraints -- I'm afraid this is quite a vague explanation but hopefully not inaccurate as a first-order clarification

[Reid Barton]

It's about the difference between "computing" (in the sense of type theorists) with terms, which may contain free variables, which is done by the kernel, and computing (in the sense of everyone else) with values, which is done in the VM or by compiled or extracted code (in other systems).

[Reid Barton]

Props are represented by nothing in the VM. Then large elimination for eq could be a problem for the VM, but since we don't have UA in Lean, we support a simple semantics in which the denotations of propositionally equal types are the same. That means that the VM never gets stuck on eq.rec expressions, and so you can use arbitrary axioms inside proofs without blocking computation.

[Reid Barton]

Or at least, this is my understanding. I'm not sure I am explaining it in a technically correct way.

[Valery Isaev]

I think I understand now. First of all, this has nothing to do with the difference between VM/native/interpreted code. So, evaluation of Lean code can be implemented using any of those options. The actual reason why Lean code can be evaluated is that all axioms leave in Prop and evaluation cannot depend on values in Prop (so, we can add any axiom to Prop, right?). I think this is also true for Coq. So, are there any differences between Lean and Coq approach to this problem?

[Reid Barton]

I don't know for sure, but I would assume there is no difference.

[Reid Barton]

Also, it's not entirely true that all axioms live in Prop: choice doesn't. However, any usage of choice that is contained in something that gets erased is not a problem for computation.

[Reid Barton]

Lean has a flag on each top-level declaration for whether it is noncomputable. I don't know if the exact rules are written down anywhere, but I think it's roughly:

• if the type T of X is erasable (T is either a proposition, or a string of Pis ending in Prop or Type) then X is always computable
• axioms are noncomputable (if their types are not erasable)
• A definition in which something noncomputable appears and isn't inside any subexpression with erasable type is noncomputable.

[Reid Barton]

Lean knows how to work this out and will complain if you forget to write noncomputable (or erronesouly write noncomputable), and the noncomputable definitions are supposed to be exactly the ones the VM doesn't know how to deal with.

[Valery Isaev]

So, I was correct when I assumed that there is a computable subset of the language. I guess you can use axioms and non-computable stuff there as long as it appears in computationally irrelevant parts (whatever that means).

[Reid Barton]

I guess the right way to express it is to say what expressions are computable, with the rules (a) all the basic parts of the language (but not axioms) are computable, (b) if $e : T$ where $T$ is erasable, then $e$ is computable.