How to represent mathematical partial functions in a type-theory based proof assistant?

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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

Answer 5

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.

Answer 6

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

Answer 7

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...

Answer 8

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.

Answer 9

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.

Answer 10

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.