6
$\begingroup$

I noticed that in Lean, the localization of rings (which is unique up to isomorphism) is defined as a predicate is_localization.

I am not an expert in Lean, and I'm not aware of much of the discussion in the Lean community. But this has led me to wonder: Since such an approach has many benefits, why don't we use that everywhere? Is it possible to define and use is_nat, is_tensor_product, etc? If not, what are the downsides that prevent this from happening?

One thing that I can think of is that Lean has built in support for inductive types, so defining natural numbers or cartesian products in this way wouldn't be worth it, since all the support (pattern matching etc.) will be lost.

As a tangential question, how well does this approach scale with other proof assistants such as Coq and Agda?

$\endgroup$

2 Answers 2

8
$\begingroup$

The question is about declarative versus computational formalization.

In the declarative style we characterize a “thing” by stating conditions, quite often universal properties, that determine it up to a unique isomorphism. Any “thing” satisfying the stated conditions is acceptable.

In the computational style we just construct the “thing” concretely, and use features provided by the proof assistant to compute with it directly.

A typical example is the structure of natural numbers. In the declarative style we define “pointed successor algebra” and say that $\mathbb{N}$ is an initial pointed successor algebra. In the computational style we define $\mathbb{N}$ as an inductive type.

Each approach has benefits and drawbacks:

  1. The declarative style is more flexible, but doing everything in this style complicates formalization. For example, one can never refer to “the natural numbers $\mathbb{N}$” but must always say “and given an initial pointed successor algebra $N$ ..." Now imagine you had to do this every time you wanted to mention a cartesian product, a function space, a unit type, etc.

  2. The computational style allows us to compute more easily (although the declarative one does as well with some extra work), but it locks in specific design choices. You defined natural numbers in unary, but now you'd like to compute in binary? Tough luck, you'll have to get the proof assistant developers to hack the system and provide some magic.

People tend to use the computational style, but there are situations which demand a different approach because the “unique up to unique isomorphism“ cannot be realized as an exact equality. For example, suppose we want to define “the $n$-th power of $A$” as a type? That's easily done:

open import Data.Nat
open import Data.Product
open import Data.Unit

module Cow where

  power : Set → ℕ → Set
  power A zero = ⊤
  power A (suc n) = A × power A n

But what if we want $A^{n + m} = A^n \times A^m$ to hold as an equality? This might be doable, but is at the very least going to require a lot of trickery and fragile design. And then someone is going to walk in and ask about $A^0 = 1$, and everything will crumble.

The Lean library defines is_localization for a similar reason. Because the “equality” $R[1/f][1/g] = R[1/f g]$ (or some such) cannot be achieved using any reasonable concrete construction of $R[1/f]$, we switch to declarative style as we have to deal with isomorphisms anyhow.

In my opinion, we are not facing just a formalization engineering problem, but rather a genuinely mathematical one. Many branches of mathematics sweep the problem under the rug by saying things like “we identify $A^{n + m}$ with $A^n \times A^m$“ – but homotopy theorists and higher-category theorists thrive on it. It remains to be seen how their insights can be transformed into formalization techniques. A very good attempt is homotopy type theory and univalent mathematics, which however requires one to pay a high price – a new way of thinking – and is therefore not very popular.

$\endgroup$
7
  • 1
    $\begingroup$ One might argue that both declarative and computational styles of formalization are each already the transformation of a higher-categorical coherence method, namely the non-algebraic and algebraic respectively. $\endgroup$ Aug 7, 2022 at 19:42
  • $\begingroup$ Yes, that is a very good observation. Formalization could benefit from such insights, so that questions of design become mathematical questions rather than experience-based methodology. Although, the insighs that will bring progress are not necessarily of the kind that higher-categorical people expect. For example, what advice could we give about the question "when do use declarative and when to use computational approaches"? $\endgroup$ Aug 8, 2022 at 9:51
  • $\begingroup$ Computational on weekdays and declarative on Sundays? $\endgroup$ Aug 8, 2022 at 18:51
  • $\begingroup$ Careful there, you already gave me a sleepless week once ;-) $\endgroup$ Aug 8, 2022 at 18:52
  • $\begingroup$ I am reminded of the last two paragraphs of this blog post. $\endgroup$ Aug 8, 2022 at 18:54
0
$\begingroup$

So in my opinion your question is basically why don't we use subset types $\{ x \colon A \mid P(x) \}$ more in proof assistants?

Unfortunately this approach tends to work best classically and not constructively. Usually you have to assume axioms like proof irrelevance or even choice principles to make this sort of approach work best. Lean has special support in the VM to make certain axioms compute at the cost of a weirder metatheory. I suppose the principle of unique choice may be a reasonable compromise for many purposes.

I suppose Coq's relatively recent support for proof irrelevant propositions might be nicer for this sort of thing?

It is worth noting while you can't prove proof irrelevance in general for many propositions you can prove proof irrelevance for specific propositions such as decidable propositions. So stuff like decidable subset types $\{ x\colon A \mid P(x) = \textbf{true} \}$ don't really face as many annoying problems.

I think it's also worth noting that this sort of approach doesn't scale more generally past the category of sets. There are many categories that just don't have a subobject classifier and so really one must make do with clunkier approaches using monomorphisms. So if you tried to go forward with this sort of style you'd end up with awkwardness like $\{ x\colon B, y\colon A \mid f(x) = y \}$.

$\endgroup$
10
  • 1
    $\begingroup$ The principle of unique choice is constructive in the sense that it can be given a computational interpretation. Could you be more precise about these usess of non-constructivism in the use of subset types, apart from proof irrelevant propostions (which are not non-constructive)? $\endgroup$ Aug 5, 2022 at 9:05
  • 1
    $\begingroup$ A subobject classifier is not necessary for subset types. Rather, you need a kind of comprehension principle. $\endgroup$ Aug 5, 2022 at 9:07
  • 1
    $\begingroup$ The principle of unique choice is valid in every topos, and in particular in the effective topos, which gives it a computational meaning via the realizability interpretation. In the same fashion, proof-irrelevance works in a topos, too. Don't judge the whole world by what Coq can do. $\endgroup$ Aug 5, 2022 at 19:20
  • 1
    $\begingroup$ Realizability has undecidable type-checking, which is definitely a problem for a foundational system. On the one hand, I think you can prove some impossibility result stating that any extension of MLTT that has both a judgmentally proof-irrelevant Prop and UC for that sort must have undecidable type-checking. OTOH, you can implement UC in Coq (while retaining decidability, since Prop is not strict) but the price you pay is that you cannot erase propositions anymore in extraction. $\endgroup$ Aug 6, 2022 at 15:16
  • 1
    $\begingroup$ @MolossusSpondee: I think your wording threw me off when you said "works better classically than constructively" and then went on describing unique choice and proof irrelevance, which gave me the impression you were linking "classical" with "unique choice" and "proof irrelevance". I should have read more carefully. $\endgroup$ Aug 8, 2022 at 18:56

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.