The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

On 4/3/20 6:52 pm, Guillaume Melquiond wrote:
> In a HOL setting (or plain FOL for McCarthy's F91), types are never
> empty, so functions always exist and return values, whether terminating
> or not. (Obviously, if they do not terminate, you will not be able to
> prove anything interesting about their return value.)

I'd call this true but misleading.  I would say that a function that 
does not terminate does not in fact exist.  If it did, we would have the 
following logical paradox (the code is SML, basically simply type theory)

(** Grelling paradox -
   a word expresses a property, which may or may not apply to that word,
   eg 'English' is an English word, 'short' is a short word,
     'French' is not a French word, 'long' is not a long word,
   define a word to be heterological if it does not truly describe itself;
   paradox : is the word 'heterological' heterological ? **)

type word = string ;
type property = word -> bool ;

(* prop : word -> property, gives the property expressed by a word
   heterological : property *)

fun prop "heterological" = heterological

and heterological wd = not (prop wd wd) ;

(* the paradox is to evaluate heterological "heterological" *)
(* heterological "heterological" ; ! Uncaught exception: ! Out_of_memory *)

Jeremy