Two questions about SMT-LIB 3 format from a knowledgeable colleague who does not use email

28 views

Martin Suda

Sep 16, 2021, 10:27:15 AM9/16/21
to SMT-LIB
1. Can types be empty in SMT3? It's hard to have dependent types
without allowing for empty types, though not impossible. Mizar does
it, but it's a very different kind of type system than CIC.

2. Is it extensional wrt types? EG, if v has type Vector (n + m) where n,m : Int, then
does it also have type Vector (m + n)? CIC does not have this property, and including
it makes type checking as hard as theorem proving.

Here are a few references everyone probably knows, but just in case:

Benjamin Werner and Peter Aczel showed how to interpret a "classical
CIC like type theory" in classical set theory (and vice versa):

Benjamin Werner. Sets in Types, Types in Sets. TACS 97.

Peter Aczel. On Relating Type Theories and Set Theories. TYPES 1998.

There's also relevant later work, e.g.:

Bruno Barras. Sets in Coq, Coq in Sets. JFR 3. 2010.

Gyesik Lee and Benjamin Werner. Proof-irrelevant model of {CC} with
predicative induction and judgmental equality. LMCS 4. 2011.

With respect to proofs, if SMT3 is really a fragment of CIC, then the
quickest way to get a preexisting notion of proof is simply to
translate the formula into a Coq/Lean type and then say the proof is
something of that type (allowing the use of classical, extensional and
choice axioms in the proof term). This won't work if types are meant
to be extensional (Question 2 above), but in that case one could still
translate to an underlying set theory (via Werner and Aczel's ideas)
and say a proof is a proof in the set theory.

Cody Roux

Sep 16, 2021, 1:01:30 PM9/16/21
to SMT-LIB
This is a question I was meaning to ask as well!

I'm pretty sure that the "usual" interpretation of fresh types in SMT is non-empty, which may make things a bit finicky.

In Lean and Coq, there is often use of a type-class "inhabited" which is defined by

Class inhabited A := { elt : A }

Then every declaration, say of a polymorphic function like nil : forall A, list A, could be guarded by this type class: nil : forall A { _ : inhabited A}, list A.

However this does create a proof obligation when defining things like inductive families.

Concerning extensionality, I don't think this comes up much in the absence of type families like Vect, which I suspect is not really high on the radar of what SMT-LIb 3 is trying to accomplish. I think it's more about having a higher-order polymorphic predicate logic with proof terms. This suggests to me that types should be extensional, and in general, not a lot of computation is expected to occur in the type checking process beyond beta and delta reductions.

Indeed, further restrictions may even be necessary if type checking is to be efficient.

Is there a reference for Mizar's model of non-empty types?

Best,
Cody