12
$\begingroup$

I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded datatypes on it, which made clearer why his extensions would be necessary.

Nether less, I'm still left wondering where those extensions came from. Why they are what they are? What justifies them? I know, for example, that some extensions, such as recursion, ruin the language as a system for proofs. If I decided to also extend CoC with other primitives, how would I justify? I understand a proof of normalization is necessary, but that doesn't prove those primitives "make sense".

In short, what specifically what qualifies a language (and its type-system) as a system capable of proving theorems about its own terms?

$\endgroup$
  • $\begingroup$ I read a blog that was related to this question, but I am unable to find it now :( It contained the sentence "System T is enough!" or something like that and it talked about dependent type systems. $\endgroup$ – Labbekak Mar 16 '18 at 8:16
  • 2
    $\begingroup$ Found it: queuea9.wordpress.com/2010/01/17/… It's actually written by Aaron Stump so you might already know about it. $\endgroup$ – Labbekak Mar 16 '18 at 8:23
  • $\begingroup$ Unguarded recursion "ruins" the language as proof system, guarded recursion does not. To prove that the primitives make sense, I'd say that you build a model. And to prove theorems about its own terms, it needs a sort of Curry–Howard isomorphism, and dependent type so that the things you prove (types) can talk about your terms. $\endgroup$ – xavierm02 Mar 16 '18 at 13:32
5
$\begingroup$

[Self-advertising follows, but I think that this is relevant.]

There are several possible approaches to this questions. One of the ways (that I explored during my PhD thesis in the context of an ML-like language) is to extend the type system with a first-order layer, so that terms of the language can be manipulated as objects of the underlying logic. Of course, you also need to include some predicates so that there is something to observe. In the case of my system, these predicates are term equivalences. In particular, if $t$ and $u$ are terms of the language, then the type $t \equiv u$ is only inhabited if $t$ and $u$ are indeed (observationally) equivalent. You can use first-order quantifiers to encode properties such as $\forall v, (\lambda x.x)\;v \equiv v$ in types, and they are proved by constructing programs inhabiting them.

Of course you can also assume equivalences, and there are several different forms of quantifiers (typed / untyped, universal / existential). This mechanism can be used to reason about any program (they do not have to be proved terminating or even typed). The only constraint is that programs that are used as proofs must be proved terminating by the system (arbitrary general recursion leads to inconsistency).

Here are a couple of references if you want to check this out:

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.