Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Say I have a program that needs to not divide by zero:

f(x):
    if nonzero(x):
        return sin(x)/x
    else:
        return 1

If we divide by zero, we get an error. We can prove that the above function does not error by noting that the first if branch is not taken when x==0, so the possible error from the division can't happen, and we always get a sensible result.

So the question is what does this proof look like in type theory?

I know it must involve dependent types and such, and I've read a few relevant Wikipedia pages, but I don't know how to type nonzero() or division or how to show in type theory that the error can't happen.

(This isn't supposed to have anything to do with zero in particular, I'm wondering in general how type theory handles proving things around such predicates and dependently-typed functions)

share|improve this question
    
For quicker answers to computer science questions, and a more computer sciency perspective than you sometimes get here, I recommend asking computer science questions on Computer Science. –  Gilles Dec 26 '13 at 2:31

1 Answer 1

This entirely depends on your type theory. Whole books have been written on type theory, and that's just the introduction before you start diving into research papers, so you can't cover all the cases.

Let's stick to compositional theories, where an expression is well-typed only when its subexpressions are, following the usual treatment of expressions with free variable (putting them in a context). In that case, there must be:

  • a type system that either has a type of nonzero numbers as a subtype of numbers, or allows typing a division with a hypothesis that the denominator is nonzero;
  • an instance of a typing rule for the if construct that allows typing the subexpression sin(x)/x in a context where $x \ne 0$.

A fairly simple type system can have the following relevant rules, where $T \le T'$ means that the type $T$ is a subtype of $T'$ and $\mathbb{R}$ is the type of reals (or computable reals, or whatever domain you're computing on): $$ \mathbb{R}^* \le \mathbb{R} \qquad \frac{\Gamma, x:\mathbb{R}^* \vdash M:T \quad \Gamma \vdash N[x\leftarrow 0]:T} {\Gamma, x:\mathbb{R} \vdash \mathtt{ifnonzero}(x, M, N) : T} \qquad \frac{\Gamma \vdash M:\mathbb{R} \quad \Gamma \vdash N:\mathbb{R}^*} {\Gamma \vdash (M/N):\mathbb{R}} $$ Sure, this is ad hoc, but it's enough to type this particular program. It isn't necessary to make the type grammar complex to handle this case.

Another syntactic approach to typing allows types to embed formula. By the Curry-Howard correspondence, types and logical propositions are essentially the same thing. A popular type theory based on this principle is the calculus of constructions. Under this approach, the division operator can take two likely forms:

  • two arguments: a real, and a real together with a proof that this real is nonzero;
  • three arguments: a real, another real, and a proof that the second real is nonzero.

In both cases, the type of the operator is a dependent type, since the type of the proof that the denominator is nonzero involves the denominator. Having a term embedded in a type is the definition of a dependent type system. Here's how the type of the division operator would look like in a Coq-like syntax, under the two approaches outlined above:

(/) : R -> {y:R | y <> 0} -> R
(/) : R -> forall y:R, y <> 0 -> R

You can explore Coq's axiomatization of the reals. This is an axiomatization, not an implementation — there's no definition of the inverse function Rinv, it is a parameter of the theory (alongside Rplus, Rmult, …). This axiomatization chooses a different, less intuitive but more convenient model: Rinv must be defined over all the reals, but it is only ever used in proofs with an assumption that implies that the denominator is nonzero. The axiom Rinv_l states:

forall r:R, r <> 0 -> (Rinv r) * r = 1

or in a more mathematical notation: $\forall r:\mathbb{R}, \neg (r = 0) \to \mathtt{Rinv}(r) * r = 1$. In this theory, the if construct has a dependent type, where the value of the boolean test can be assumed when typing the alternatives. $$ \frac{\Gamma \vdash C : \mathtt{boolean} \quad \Gamma, H:C=\mathtt{true} \vdash M:T \quad \Gamma, H:C=\mathtt{false} \vdash N:T} {\Gamma \vdash \mathtt{if}(C,M,N) : T} $$ This isn't the actual rule, but an presentation which is as close as I can get without a 10-page treatise on dependently-typed pattern matching. I'm also passing over the distinction between syntactic equality and semantic equality, and between equality testing (a boolean-valued function) and the equality predicate (a proposition), which quickly becomes apparent if you actually try to play with this in Coq.

Given the expression if nonzero(x)…, the condition $C$ is $x \ne 0$, which can be used to prove that the subexpression $\mathtt{sin}(x)/x$ is well-formed, and thus that the whole expression never requires a division by zero.

Yet another approach to typing is to treat types as set. This approach tends to appeal to mathematicians, but not to compiler writers, because sets and algorithms don't mesh well. Under this approach, the alternatives of the conditional constructs assume the condition or its negation in addition to the other ambient assumptions. $$ \frac{\Delta \wedge C \Vdash M \in T \quad \Delta \wedge \neg C \Vdash N \in T} {\Delta \Vdash \mathtt{if}(C,M,N) \in T} $$

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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