18
$\begingroup$

Isabelle/HOL’s logic is called a logic of “total functions”, yet there are functions that are obviously not total, such as division div.

How does this make sense?

$\endgroup$
6
  • $\begingroup$ Should I just try to answer my own question, based on joachim-breitner.de/blog/…, or does it look better for a stack exchange beta if someone else answers? $\endgroup$ Commented Feb 9, 2022 at 8:56
  • 4
    $\begingroup$ Self-answering is encouraged $\endgroup$
    – Glorfindel
    Commented Feb 9, 2022 at 8:58
  • 1
    $\begingroup$ @Glorfindel While this is a general SE policy, I think it is fair to let the community decide whether they wish it to be the case on this site. I have created a relevant Meta thread for this discussion. $\endgroup$
    – Wojowu
    Commented Feb 9, 2022 at 16:18
  • $\begingroup$ @TheAmplitwist, don’t you like my typographic quotes that you edited them to ASCII-ones? $\endgroup$ Commented Feb 10, 2022 at 9:23
  • 1
    $\begingroup$ @JoachimBreitner Oh, I did? I beg your pardon. That was unnecessary on my part, there's no problem with typographic quotes at all. The main thing I intended to edit was the title, and the last sentence in the body. Perhaps I edited the quotes on reflex, I'll avoid doing that in the future. $\endgroup$
    – user158
    Commented Feb 10, 2022 at 10:10

1 Answer 1

17
$\begingroup$

If you have a Isabelle/HOL function f :: a ⇒ b between two types a and b (NB: the function arrow in Isabelle is , not ), then – by definition of what it means to be a function in HOL – whenever you have a value x :: a, then the expression f x (i.e. f applied to x) is a value of type b. Therefore, and without exception, every Isabelle function is total.

This has a few consequences when modeling functions that are commonly considered partial.

  • In some cases, like subtraction on naturals, the function is made artificially total by returning a particular value: 0 - 1 = 0.

    This may look fishy at first, but it is ok (theorems about subtraction that don’t hold for the extended version will have necessary preconditions) and useful (a fair number of theorems do hold, and can be used without having to discharge such preconditions).

  • In other cases the partial function takes on an arbitrary, but unspecified and unknown value.

    Consider the Eps :: "('a ⇒ bool) ⇒ 'a" operator, which models choice. When the predicate P is true for some x, then Eps P is one of these, and P (Eps P) holds (∃x. P x ⟹ P (Eps P) is a theorem). But nothing stops you from using Eps with a never-true predicate, e.g. Eps (λ n, n = n + 1) :: nat. This is a value of type nat, but you don’t know which one, and no useful theorems are provided for it.

    Similarly, the undefined :: 'a term is a value of any type, and again one that you don’t know anything about.

  • Relatedly, in HOL all types are inhabited – for example by the undefined above. This is crucial for the tricks shown above, and otherwise not a big deal either – in contrast to Logics based on Type Theory, which conflate types with propositions, and inhabited types with theorem.

I wrote a longer text on partiality and definedness of Isabelle/HOL function.
$\endgroup$
1
  • 3
    $\begingroup$ I think the last point is the most surprising one for people coming from dependent type theory, which has lots of uses for empty types besides propositions-as-types: the type of real numbers that squares to -1 is empty, the empty type is the initial object of the category of types, the empty type is the type of free variables allowed in a closed sentence in FOL, etc. $\endgroup$ Commented Feb 10, 2022 at 10:45

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.