Nikola Katić (Nov 10 2022 at 13:07): Nikola Katić (Nov 10 2022 at 13:07):Hello :wave: There is a quote from the "Concrete semantics" book:
HOL is a logic of total functions, hd [] is defined, but we do not know what the result is. That is, hd [] is not undefined but underdefined
Can someone clarify difference between those notions?
Robert Soeldner (Nov 10 2022 at 13:09):Hi, there is a really good blog post here: https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined
Nikola Katić (Nov 10 2022 at 13:26):I hoped there is a more direct explanation :smile: After skim reading it, I saw comparisons with Coq and Haskell, which is nice, since I have some background in those. I'll definitely save it and read it carefully. Thanks for the article!
Manuel Eberl (Nov 10 2022 at 17:23):Well, the short answer is: ‘undefined’ suggests that hd [] is something that we are not even allowed to write down. And that perhaps we can test whether or not hd [] is defined or not. But we can't.
Manuel Eberl (Nov 10 2022 at 17:24):Rather, the situation is such that we know that hd ([] :: nat list) is some natural number, but we don't know which one it is. So in that sense, the hd function is underdefined. The system gives us some function nat ⇒ nat list, and for non-empty lists we know exactly what it is, but for the empty list as an input we know absolutely nothing (other than that it will be some natural number).
Mathias Fleury (Nov 10 2022 at 17:28):Jasmin once described it to me along the lines of: "hd [] has a value, but it changes every time Isabelle restarts"
Manuel Eberl (Nov 10 2022 at 17:33):haha, that's a good one. :smile:
Manuel Eberl (Nov 10 2022 at 17:34):The value of hd [] is only available with Isabelle Professional or Isabelle Enterprise Edition.
Wolfgang Jeltsch (Nov 10 2022 at 18:54):Mathias Fleury said:
Jasmin once described it to me along the lines of: "
hd []has a value, but it changes every time Isabelle restarts"
Well, I think this explanation is misleading; the underdefinedness has nothing to do with Isabelle runs. I rather see it like this: The HOL theory (what you get if you use Isabelle/HOL) is just a theory; it gives only logical statement about what holds and what not. This theory can have several models: several assignments of concrete values to variables like hd. With one model hd [] :: nat is 0, with another one it is 1000, and so on. All these different models (different “definitions” of hd) are compatible with what Isabelle/HOL states.
Wolfgang Jeltsch (Nov 10 2022 at 18:59):I think the core of my message is this: In a functional programming language, like Haskell, you always define variables. For example, you say what head (Haskell’s equivalent of Isabelle’s hd) is: head [0], for instance, is 0 and head [] is ⊥, a special value that is of the natural number type, but is different from any true natural number. In Isabelle, on the other hand, you provide an, often partial, specification of properties of your variables. For example, you say that hd [0] is 0, but you say absolutely nothing about hd []. It must be one true natural number (as there is no ⊥), but it is simply not known which one it is.
Mathias Fleury (Nov 10 2022 at 19:00):Wolfgang Jeltsch said:
Mathias Fleury said:
Jasmin once described it to me along the lines of: "
hd []has a value, but it changes every time Isabelle restarts"Well, I think this explanation is misleading; the underdefinedness has nothing to do with Isabelle runs. I rather see it like this: The HOL theory (what you get if you use Isabelle/HOL) is just a theory; it gives only logical statement about what holds and what not. This theory can have several models: several assignments of concrete values to variables like
hd. With one modelhd [] :: natis0, with another one it is1000, and so on. All these different models (different “definitions” ofhd) are compatible with what Isabelle/HOL states.
Yeah, but you within one isabelle run, the value is constant (hd ([]::'a list) = hd ([] :: 'a list)). You need a restart for the value to change. Hence it has something to do with Isabelle runs.
Mathias Fleury (Nov 10 2022 at 19:01):although you are right and it has nothing to do with isabelle runs
Wolfgang Jeltsch (Nov 10 2022 at 19:03):Note that the approach of using “underdefinedness” has some interesting consequences. Take undefined which has the polymorphic value 'a and for each concrete type is some value about which we don’t know anything (the name might be misleading, specifically if you come from Haskell). You can prove the statement undefined = False ∨ undefined = True ('a being specialized to bool via type inference here), but you don’t know which of the booleans it is. Also, you can prove undefined = undefined, because in each concrete model there is a concrete undefined (otherwise, referential transparency wouldn’t hold), but if you defined another constant, say undefined', about which you don’t say anything, then undefined = undefined' wouldn’t be provable.
Wolfgang Jeltsch (Nov 10 2022 at 19:18):Yeah, but you within one isabelle run, the value is constant (hd ([]::'a list) = hd ([] :: 'a list)).
My view is different: There is just not the value of hd, not even within a single Isabelle run. There is a set of permissible assignments of concrete values to the constants of the HOL theory (like hd). However, the statement (hd ([]::'a list) = hd ([] :: 'a list) is still true, because being true means being true for each particular permissible assignment, and each particular assignment has a single value for hd [].
Note that this view has an advantage when it comes to contradictions, which you can introduce when stating axioms. Say you write the following:
axiomatization where contradiction: "hd [] = 0 ∧ hd [] = 1"
What value does hd [] have now for you current Isabelle run? There can’t be any. However, it is still true that, for example, (hd ([]::'a list) = hd ([] :: 'a list) holds for every model of your theory: there is just no model of your theory; so any statement holds.
Jasmin Blanchette (Nov 14 2022 at 12:04):Mathias Fleury said:
Jasmin once described it to me along the lines of: "
hd []has a value, but it changes every time Isabelle restarts"
Can't remember saying that! :)
Last updated: Dec 21 2024 at 16:20 UTC