15
$\begingroup$

For example, if I want to define multiplication inverse on the rational type, intuitively we would define:

÷ : Q -> <Q \ {0}> -> Q

But how would I remove a zero from the second argument?

One solution would be to add an extra parameter ÷ : Q -> (q : Q) -> q ≠ 0 -> Q, but this makes the signature ugly as it's no longer a binary function, so we cannot use, say, binary operator syntax for it.

$\endgroup$
6
  • $\begingroup$ Actually this is not an ugly signature but one form of predicative mathematics :-) The other way around in HoTT is to include Path constuctor with this restruction into datatype of Q. $\endgroup$ Feb 15, 2022 at 21:02
  • $\begingroup$ Related question $\endgroup$
    – Wno-all
    Feb 15, 2022 at 22:35
  • 1
    $\begingroup$ Q → (Σ(q:Q) q≠0) → Q is binary and can be used as an infix operator. (I am just teasing.) $\endgroup$ Feb 16, 2022 at 17:45
  • $\begingroup$ Actually Q → (q : Q) → q ≠ 0 → Q is binary as well, it's just that it doesn't return a number. (Still teasing, sorry I couldn't help myself.) $\endgroup$ Feb 16, 2022 at 17:59
  • $\begingroup$ @AndrejBauer it is either unary or ternary, depending on your criteria. $\endgroup$
    – ice1000
    Feb 16, 2022 at 18:14

10 Answers 10

11
$\begingroup$

A commonly used approach to keep things simple is to define a function Q -> Q -> Q which returns the same result as the partial function for covered argument values and returns some arbitrary result for all other argument values. The constraints on the arguments are then only used when proving the properties of the resulting function. For example, division by zero can be defined to return zero and then constrained in theorems like y <> 0 -> x / y * y = x.

$\endgroup$
9
  • $\begingroup$ Is there any version of this that works for fields like the real numbers that don't have decidable equality? $\endgroup$ Feb 16, 2022 at 1:19
  • $\begingroup$ I don't think this approach requires decidable equality. You should still be able to construct a proof of inequality for most cases. The constraint also does not have to use equality. It can be any predicate. $\endgroup$
    – Ihar Bury
    Feb 16, 2022 at 8:23
  • $\begingroup$ @Ihar: You cannot define a total function that extends the inverse function without further assumptions, such as excluded middle (which of course makes equality decidable). $\endgroup$ Feb 16, 2022 at 17:32
  • $\begingroup$ @AndrejBauer: You won't be able to use the constraint in the definition (for example, to extend an already defined partial function requiring the constraint). But in most cases you should still be able to define the total function without using the constraint. $\endgroup$
    – Ihar Bury
    Feb 16, 2022 at 18:30
  • 1
    $\begingroup$ There is no function $f(x)$ such that $xf(x) = 1$ on $\mathbb R\backslash \{0\}$ and is defined on all of $\mathbb R$ in a Brouwerian type theory, and you can actually prove this statement. $\endgroup$
    – Trebor
    Feb 19, 2022 at 14:38
16
$\begingroup$

Another possibility would be to take the result of division to lie in 1-dimensional projective space over Q. Since Q has decidable equality, we have $P^1(Q) \cong Q + \{\infty\}$, so as a set this is isomorphic to option Q as in Bjørn's answer. But this viewpoint has more mathematical meaning, and generalizes better to fields without decidable equality like the real numbers.

$\endgroup$
1
  • $\begingroup$ Doesn't this definition still run into trouble on 0 / 0? $\endgroup$ May 10, 2022 at 11:45
8
$\begingroup$

Partial functions actually have a very nice type theory of their own!

The category of sets and partial functions is (classically) equivalent to the category of pointed sets (you can think of the point as a null value) and point-preserving functions.

This is a monoidal closed category, which additionally has all finite limits and colimits (such as products and sums). The monoidal structure $A \otimes B$ corresponds to pairs of $A$ and $B$, such that it is only non-null if both components are non-null, which means that the tensor product has a diagonal map, making this a model of relevant logic. This category also has an adjunction with $\mathrm{Set}$, with the forgetful functor $U : \mathrm{Set}_\ast \to \mathrm{Set}$ just forgetting the point, and the free functor $F : \mathrm{Set} \to \mathrm{Set}_\ast$ being the map $F(X) = (\mathsf{option}\,X, \mathsf{None})$.

This adjoint setup is interpretable in a dependent type theory, using a syntax in the style of my 2015 paper Integrating Linear and Dependent Types. The main changes from that paper is that the "linear" part of the language should support contraction, and there should be a constant $\mathsf{null}_A$ which identifies the distinguished missing value.

This kind of thing actually illustrates a weakness of modern proof assistants. One of the lessons of categorical logic is that it is nice to work in an internal logic as much as one can, but our proof assistants make applying this lesson more difficult than it ought to be.

$\endgroup$
1
  • $\begingroup$ So taking the example of division above you could have $\mathbb{Q}_0 \otimes \mathbb{Q}_0 \rightarrow \mathbb{Q}_0$ so $x/0$ is not permissible for $x \ne 0$ and $0/0 = 0$. Also you need to work internally in the relevance logic. Also the adjoint stuff reminds of call by push value. I need to read your paper more closely. I agree theorem provers ought to give more power to edsls. $\endgroup$ May 7, 2022 at 0:22
6
$\begingroup$

I have written an entire blogpost on this topic, outlining a variety of solutions: https://lawrencecpaulson.github.io/2021/12/01/Undefined.html

$\endgroup$
4
$\begingroup$

It's not necessarily the best solution but in Lean you can use option types and partial (part) types. So it could be

+ : Q -> Q -> option Q

where a : option Q is either none or some b where b:Q.

$\endgroup$
7
4
$\begingroup$

Here is yet another option, which will require rethinking how $\mathbb{Q} \smallsetminus \{0\}$ is defined. Namely, suppose we think of the nonzero rationals not as the set of rationals which do not equal zero, but rather as the set of units of $\mathbb{Q}$. This can be formalized as the structure with two fields, say $a$ and $b$, both terms of $\mathbb{Q}$, along with a proof, say $h$, that $a \cdot b = 1$.

You can then define the division function $\mathbb{Q} \to \mathbb{Q}^\times \to \mathbb{Q}$ as the map sending $x$ and $(a,b,h)$ to $x \cdot b$.

This has the benefit of working over any ring (assuming the units are properly defined, which requires an additional hypothesis in the noncommutative case). But in order to obtain the original goal, one would have to identify $\mathbb{Q}^\times$ with $\mathbb{Q} \smallsetminus \{0\}$. This doesn't solve the issue of the binary operation, but certain proof assistants (e.g. Lean4) have support for heterogeneous operations.

Here is a formalization of this in Lean4 (for any monoid), including a use of heterogeneous division for nice syntax:

class Monoid (α : Type u) extends Mul α, OfNat α (nat_lit 1) where
  mul_assoc (a b c : α) : (a * b) * c = a * (b * c)
  one_mul (a : α) : 1 * a = a
  mul_one (a : α) : a * 1 = a

structure Units (α : Type u) [Monoid α] := 
(u v : α)
(huv : u * v = 1)
(hvu : v * u = 1)

instance (α : Type u) [Monoid α] : HDiv α (Units α) α where
  hDiv := λ a b => a * b.v

example (α : Type u) [Monoid α] (a : α) (b : Units α) : α := 
  a / b
$\endgroup$
4
$\begingroup$

This is starting to be a party of solutions! There are several monadic solutions to this problem beyond the Option/Maybe monad suggested by Bjørn. Perhaps monads aren't that scary to people around here but I will nevertheless explain the idea plainly, focusing on the underlying mathematics first rather than on the computer science.

To make this concrete, let's look at this equation: $$\frac{x^2 - y^2}{x+y} = x-y$$ This is evidently true but when we do that we implicitly ignore the problematic case where $x+y=0$. There is no type theory that I know which includes "implicitly ignoring". So we have to look a bit deeper into what we really mean by the equation above.

The first step is to think about what $x$ and $y$ mean. The key is to think of them as projections. Without any further constraints or additional context, we can think of $x$ and $y$ as the first- and second-coordinate projections $\mathbb{Q}^2 \to \mathbb{Q}$. Then an equation like $x + y = y + x$ is simply a map from $\mathbb{Q}^2\to\mathsf{Prop}$, and a proof of this identity is a proof that this is the constant map with value true. This allows us to easily make sense of any total operations like addition, multiplication, negation.

We can also make sense of division in this way but we need to enrich the context. Our equation $$\frac{x^2 - y^2}{x+y} = x-y$$ doesn't make sense as a function from $\mathbb{Q}\times\mathbb{Q}\to\mathsf{Prop}$. However, there is a two-dimensional variety over which it makes perfect sense, namely the variety $$V = \{(x,y,z) \in \mathbb{Q}^3 \mid (x+y)z = 1\}$$ If we think of $x$ and $y$ as the first- and second-coordinate projections $V \to \mathbb{Q}$ then $$\frac{x^2 - y^2}{x+y} = x-y$$ makes perfect sense and a proof of this identity is a proof that this equation defines a constant map $V \to \mathsf{Prop}$ with value true.

Where's the monad? It's in the variety $V$. This is known as a Reader monad. In general, the Reader monad is used to share an environment or context between values. In this case, the shared context is the variety $V$ and $x,y,z$ are not values but maps $V \to \mathbb{Q}$. A proof assistant with strong support for monads can automate keeping track of the contextual variety $V$ and can make large parts of this process relatively seamless.

Besides being correct, there are some advantages to working with such monads. To an algebraist, the question whether $$\frac{x^2 - y^2}{x+y} = x-y$$ is true on the variety $V$ probably wouldn't be a direct proof that this is a constant function. Rather, the algebraist would probably ask whether the congruence $$(x^2-y^2)z \equiv x - y$$ holds modulo the ideal generated by $(x+y)z - 1 = 0$. There are many sophisticated tools available to automate this type of questions...

$\endgroup$
2
  • $\begingroup$ This is actually closely related to Mike's solution too. And it also doesn't rely on decidable equality, except perhaps in the automation part suggested in the last paragraph. $\endgroup$ May 4, 2022 at 7:27
  • $\begingroup$ Also note that Adam's solution is the same except that the additional variable $z$ in the variety $V$ is coded into the Units structure. $\endgroup$ May 4, 2022 at 7:34
3
$\begingroup$

Use a definite description operator

I believe you want an isomorphism

$$ \exists! x\colon A. P(x)\cong P(\iota x\colon A. P(x)) $$

Then define

$$ y/x := \iota z. (\mathop{\text{Some}} z = y \mathbin{\text{div}} x) $$

Not sure of any theorem provers with really great support for definite description though.

I'm aware of stuff like Coq's but it's an axiom and doesn't compute.

$\endgroup$
6
  • 1
    $\begingroup$ Definite description is not computable in general, much like axiom of choice. There's nothing that prevents us from defining f(x) := "the y in {0, 1} such that y = 1 iff the Turing machine encoded by x halts"... $\endgroup$ May 6, 2022 at 23:28
  • 1
    $\begingroup$ @ZhanrongQiao So I guess you'd want { x: A | P(x) } -> unique P -> P(iota x: A, P(x) instead of exists! x: A. P(x) -> P(iota x: A. P(x)). Either that or make the predicate a Prolog like horn clause or at least decidable. Do those sound like options that would work? $\endgroup$ May 6, 2022 at 23:54
  • 1
    $\begingroup$ If you could make a decidable witness for P, that indeed works, but in this case it seems to me that a special mechanism for definite description is no longer necessary. I guess you'd simply use the function f that generates the witness (instead of using iota operator), and prove a lemma ∀ x: A. (P(x) <-> x = f) (showing uniqueness)? $\endgroup$ May 7, 2022 at 9:38
  • 1
    $\begingroup$ (I feel like iota is useful only when you can't really write down an explicit formula for the witness...) $\endgroup$ May 7, 2022 at 9:46
  • 1
    $\begingroup$ @ZhanrongQiao so context why I might be interested in a whacky version of definite description would be to work around a lack of definitorial expansion proofassistants.stackexchange.com/questions/1349/… . Not very useful for the sort of use with division anymore though. $\endgroup$ May 7, 2022 at 17:00
3
$\begingroup$

I believe a good way to do this is to change the type to something like:

$$ \div:(a ~ b:F) \to (b \ne 0 \times F) \sqcup b = 0 $$

I believe this gives the maximal information.

Another (crude and ineffective) way to do it is to use dependent types. Define the following dependent type (this is pseudocode):

Div : Q -> Type
Div 0 = Unit
Div _ = Q

Then, we do ÷ : Q -> (q : Q) -> Div q and this is a dependent type. Trying to divide with zero will not get you a number, and the function is still binary.

$\endgroup$
2
  • 3
    $\begingroup$ Note that a definition of Div by pattern-matching only works if 0 is a constructor of Q. More generally, since the rationals Q has decidable equality, you can define Div by casing on that. But if you want to define division on the real numbers, say, this isn't available (unless you're assuming excluded middle). In general you can replace the output by the "partial map classifier", but that that isn't much of an improvement over adding q ≠ 0 as a hypothesis, since the elements of the partial map classifier are functions. $\endgroup$ Feb 15, 2022 at 21:25
  • 2
    $\begingroup$ It seems as though this might just move the problem around as well. In a situation where q is obviously (to the computer) not 0, there are techniques for eliding the evidence. In situations where that wouldn't work, this function would produce an opaque result that couldn't be used unless coupled with the same evidence, and might actually less convenient in such cases. $\endgroup$
    – Dan Doel
    Feb 17, 2022 at 0:33
1
$\begingroup$

Here's a pragmatic answer, rather than theoretical, if you're working in Idris2 or Agda.

In Idris, you can define this as (÷) : Q -> (q : Q) -> {auto pf : q ≠ 0} -> Q. Then, you can write x ÷ y as a binary operation with no issues, and you don't get visual overhead.

For Idris, I wouldn't use q ≠ 0, I'd define something like: data NotZero : Q -> Type where nz : NotZero (S q)

Auto search will have a much easier time, I think, detecting that. Of course, I'm not sure how you're representing Q, so it might not be so simple.

In Agda, you can do something similar with tactic-implicit arguments: _÷_ : Q -> (q : Q) -> {@(tactic someTactic) : q ≠ 0} -> Q. This is not quite as easy as Idris, because you either need to write or find a tactic that finds the proof. But it's more flexible, i.e. you can probably write a tactic to solve for the actual negation (q ≡ 0 -> ⊥).

In both cases, if the tactic/auto-search fails to find a proof, you can always supply one manually, at the cost of losing your nice binary operation syntax.

$\endgroup$

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.