Typing proof trees or proof objects

Question

Is there a theory of typing proof objects or proof trees?

Partially inspired by this question and answer, I was wondering about separating type checking into two phases: the first phase infers a full proof tree and the second phase checks if the proof tree is well formed and conclusions follow from premises.

Potentially, this sort of separation allows a smaller kernel. Also the kernel can be written as a total function within a prover of similar power without extra axioms. I think it's the driver which infers the proof trees which would require extra axioms.

What I mean is you can provide explicit witnesses for typing judgements.

For the STLC, something like this:

$$\frac{\begin{split} q_0 \colon [ \Gamma \vdash e_0 \colon \tau_0 \rightarrow \tau_1 ] \\ q_1 \colon [ \Gamma \vdash e_1 \colon \tau_0 ] \end{split}}{ q_0 q_1 \colon [ \Gamma \vdash e_0 e_1 \colon \tau_1 ] } $$

$$\frac{q \colon [ \Gamma , x \colon \tau_0 \vdash e \colon \tau_1 ]}{ \lambda x \colon \tau_0. q \colon [ \Gamma \vdash \lambda x \colon \tau_0 . e \colon \tau_0 \rightarrow \tau_1 ] } $$

$$\frac{x \colon \tau \in \Gamma}{ x \colon \tau \in \Gamma \colon [ \Gamma \vdash x \colon \tau ] } $$

The meat and potatoes is when you have more complicated features like dependent types. You'd want explicit witnesses for judgemental equalities something like:

$$ \frac{\begin{split}q \colon [ \Gamma , x \colon \tau \vdash e \colon \tau' ] \\ q' \colon [ \Gamma \vdash \colon e' \colon \tau ]\end{split}}{\beta(x \colon \tau \mathrel{:=} q' , q) \colon [ \Gamma \vdash (\lambda x\colon \tau. e) e' \triangleright_\beta [x \mathrel{:=} e'] e ]} $$

$$ \frac{\begin{split} q \colon [\Gamma \vdash \tau \equiv \tau'] \\ q' \colon [\Gamma \vdash e \colon \tau] \end{split} }{ \textbf{J}(q, q') \colon [ \Gamma \vdash e \colon \tau' ]} $$

Anyhow, it quickly gets very redundant, confusing and unreadable.

I'm confused about several aspects of this.

1. You want proof trees to be trivial to check but you also want them to not be redundant. What should it mean for it to be "trivial" to infer a property of the root of the proof tree like the environment or type?

2. It's really confusing to notate proof trees. Is there a better way of writing this silliness?

3. Are there existing references or work in this direction?

4. It's hard to come up with a reasonable meaning for proof trees. I guess you can see them as terms annotated with explicit environments and types?

Answer 1

What you are describing already happens to a large extent in a proof assistant with a trusted kernel.

Side remark: I prefer to say "derivation" instead of "proof tree" because derivations need not be about proofs, they can also be about constructions.

User input typically requires elaboration to a more explicitly annotated type theory (the process of elaboration is intertwined with the process of type-checking), let us call it the core type theory. The core type theory is designed in such a way that the judgements already encode the proof trees, except for judgemental equalities.

For example, in the simply-typed $\lambda$-calculus with explicitly annotated types of variables ($\lambda (x : A) . e$ instead of just $\lambda x . e$), the derivation of $\Gamma \vdash e : A$ can be read off immediately from $e$. There is no point in storing any extra information anywhere, as it is all there already. One only has to process $e$ to either reconstruct the derivation or decide that $e$ does not encode a valid one. This is the meaning of “terms as proofs”.

Proofs of judgemental equalities are typically not recorded for two reasons:

• They are proof irrelevant: it does not matter which proof is provided, as long as there is one. Consequently, if we have the means to reconstruct them when they exist, we need not store them.

• It is often deemed that derivations of judgemental equalities are too large to be stored. Instead, the core type theory is designed to have decidable equality checking so that the missing derivations can be reconstructed algorithmically. In a sense we are storing the derivations in time rather than in space.

To specifically address your questions:

1. There are techniques for making derivations less redundant, such as bidirectional type-checking which synthesizes some information. You are correct that redundant information is a nuisance because we need to check that the redundant copies agree.

2. With the exception of judgemental equalities, the derivations are already encoded by the terms, at least when the core type theory is explicit enough. (See the notion of standard type theory in the reference given in the next point.)

3. The idea that the derivation is directly reconstructible from the proof terms is manifested as an inversion principle, see Theorem 3.24 in Finitary type theories with and without contexts by Philipp Haselwarter and myself, and the subsequent paragraph.

4. As already said, when the theory is nice enough the derivation is encoded by the judgement, so its meaning can be taken to be the same as the meaning of the judgement. If the theory is not nice enough, then there is another theory which is nice enough that covers the original one, in which case the meaning of the former can be derived from the meaning of the latter. This is the point of the Elaboration theorem in Chapter 10 of Anja Petković Komel's doctoral dissertation.