13
$\begingroup$

The Markov's principle states that if a Turing machine does not run forever, then it halts. Equivalently, if I have a function $f : \mathbb N \to \mathrm{Bool}$, such that I have proved that $\neg\neg \exists n. f(n)=\mathrm{true}$, then I can find $\exists n. f(n)=\mathrm{true}$.

This principle is sometimes considered as constructively valid, since we can give a program that just enumerates $\mathbb N$ and searches for the solution, and if our meta-logic is classical, we can see that this program halts, which means that it is constructively true for each concrete function $f$.

What are the best practices to incorporate this principle into various proof assistants? The most naïve approach is, of course, assume it as an axiom. But I would also like to have computational properties. So for each concrete function $f$, I can do this in Agda:

f : Nat -> Bool
f = blah blah

f-good : ¬ ¬ ∃[ x ∈ Nat ] f x ≡ true
f-good = blah blah

private
  {-# TERMINATING #-}
  helper : Nat -> ∃[ x ∈ Nat ] f x ≡ true
  helper n with f n in eq
  ... | true = n , eq
  ... | false = helper (suc n)

magic : ∃[ x ∈ Nat ] f x ≡ true
magic = helper 0

I have to seal helper as private, because it indeed does not terminate on some input. But given f-good, we can be (meta-classically) sure that magic will halt.

However, this has some drawbacks:

  • If the normalization strategy is wrong, then this program will not terminate. For instance, if Agda chose to first fully expand all the branches before picking one, then it will keep entering the false branch.
  • If I try to state the general Markov's principle instead of on concrete $f$'s, then Agda will indeed loop in certain cases.
  • I might accidentally make some unsafe leaks.

Is there any better way of doing this? Also, is there any proof assistant that actually supports this with a flag or something?

$\endgroup$

1 Answer 1

16
$\begingroup$

There are different ways to implement Markov's principle, and they're not equivalent. I know of at least three techniques to implement MP.

MP as a loop

I personally find this to be a hack inherited from untyped realizability. As you observed already, it breaks the good metatheoretical properties of your system, in particular strong normalization. It also requires some form of MP in the metatheory, which is not a blocker but not great either. I guess that if your favourite proof assistant is some variant of PRL this is not so much a problem, but if you only swear by MLTT this is not going to do the job.

MP via Dialectica

It is well-known that the Dialectica interpretation realizes MP. The underlying implementation is very different from an unbounded loop. Morally you can picture it as some form of delimited continuations triggered by the access to bound variables in the calculus. I wrote a Dialectica model of CoC in my PhD, and we have an unpublished account of a Dialectica model of MLTT with Andrej Bauer, but it's not very implementable. It relies on a structure of finite multisets that enjoy definitional equations and it is not even clear we can get a decidable type system out of it.

MP by static exceptions

The third technique is, I believe, a simplification of the Dialectica approach that is easy to explain computationally and implement. Essentially, it consists in adding a special kind of exceptions to the ambient type theory. In order to preserve consistency you have to forbid exceptions at toplevel though, and ensure that they are always statically caught.

There are two ways to understand this, either in direct style or through a program translation. These two papers only handle a weak logical system, but the technique can actually be lifted to MLTT.

The resulting theory can be described as the composition of an exceptional model with a strict presheaf model. Both processes are relatively simple compilation phases so in the end you can just compile away MLTT + MP into a reasonable variant of MLTT. The result is described in this paper.

Since the presentation is synthetic, you can actually dump the syntactic model phase altogether and simply add the corresponding combinators with the reduction rules inherited from the underlying computational model. Dynamic exceptions are fairly easy to add through rewrite rules so I guess it is only a matter of correctly implementing the static try-catch handlers.

$\endgroup$
9
  • $\begingroup$ "Autem P = NP, cujus rei demonstrationem mirabilem sane detexi. Hanc marginis exiguitas non caperet." - Haha good one $\endgroup$
    – Couchy
    Mar 10, 2022 at 16:28
  • $\begingroup$ "In order to preserve consistency you have to forbid exceptions at toplevel though, and ensure that they are always statically caught." − Can you elaborate? Why would it be meaningful to have MP everywhere else except "at toplevel", and is there a proof that this ensures consistency relative to some well-known system like ZFC? Does it also ensure $Π^1_1$-soundness? Finally, I don't understand your "only swear by MLTT" remark; how can we be confident that MLTT is sound? $\endgroup$
    – user21820
    Mar 26, 2022 at 12:16
  • $\begingroup$ The model shows that CIC + MP is consistent relatively to CIC + SProp + UIP, which is itself showed to be consistent using the standard Set model (i.e. ZFC + countably many universes). Anyways, MP is already trivially true in the Set model as a consequence of classical logic so the whole point of the paper is about computation, not logical consistency. $\endgroup$ Mar 27, 2022 at 13:10
  • $\begingroup$ Exceptions being forbidden at toplevel is not related to MP. It is just that if you have unbounded dynamic exceptions in a type theory, you are trivially inconsistent. Just raise an exception to prove False, this will always be a correct term. Internally, this implementation of MP uses a special kind of exceptions that are guaranteed to never reach toplevel so as to ensure consistency. In this sense, it is essentially a form of strongly typed delimited control. $\endgroup$ Mar 27, 2022 at 13:13
  • 1
    $\begingroup$ Computation doesn't care about any of those properties. Actually, most of the time literally no property from this triple holds for your run-of-the-mill programming language. In any case, in the presheaf model one inherits from whatever computational content you have in the target, so if you put a completely platonistic set theory there you'll get a completely platonistic theory in the output. Some axioms added by forcing simply can't be realized if you're computational enough. $\endgroup$ Dec 17, 2023 at 19:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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