Email Gateway (Aug 19 2022 at 13:06): Email Gateway (Aug 19 2022 at 13:06):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi people, and Merry Christmas to all of you for whom that matters,
I know I should know, but I don't know, so the question: Isabelle
documentation often refers to sorts, something I've never bothered about
so far. Is this the same as what Wikipedia describes as being sorts in the
context of second order logic?
http://en.wikipedia.org/wiki/Second-order_logic
Quote:
Is that the relevant definition of sorts? And the second point in the
list, is that what Isabelle names arities?
Email Gateway (Aug 19 2022 at 13:06):From: Lawrence Paulson <lp15@cam.ac.uk>
Christmas greetings to you too!
Sorts regulate polymorphism, which is necessary in the case of Isabelle, since unconstrained polymorphism would break the logical framework. More details here:
http://www21.in.tum.de/~nipkow/pubs/jfp95.html
Larry Paulson
Email Gateway (Aug 19 2022 at 13:06):From: Christian Sternagel <c.sternagel@gmail.com>
Marry Christmas,
the short answer to your question is: no, what the Wikipedia article
describes is not called "sorts" (but "types") in Isabelle/HOL.
As Larry already said, sorts control polymorphism. More specifically
sorts are linked to Isabelle's axiomatic type classes. (See also the
fine tutorial on type classes that is part of Isabelle's documentation.)
E.g., you might want to prove something for all "entities" that support
some operator, say "plus", that satisfies associativity. This you might
encapsulate into a type class
class plus_assoc =
fixes plus :: "'a => 'a => 'a"
assumes assoc: "plus x (plus y z) = plus (plus x y) z"
Now by saying that something "is of sort plus_assoc" we mean that it "is
an instance of the class plus_assoc", which in turn means that it "has
an operator plus that is associative". For example, we could prove that
natural numbers are an instance of class plus_assoc:
instantiation nat :: plus_assoc
begin
definition "plus_nat (x::nat) y = x + y"
instance by (intro_classes) (simp add: plus_nat_def)
end
Now we can use "plus" on natural numbers
term "plus 0 (Suc 0)"
hope this helps
chris
Email Gateway (Aug 19 2022 at 13:06):From: Yannick <yannick_duchene@yahoo.fr>
Indeed, a short answer is on page 2:
Email Gateway (Aug 19 2022 at 13:08):From: Makarius <makarius@sketis.net>
In logic literature there is a general shortage of words for things that
qualify other things. So "type", "class", "sort", "kind", "mode" etc.
occur with varying meaning, depending on the context and the author.
In Isabelle/Pure, a sort is just a syntactic representation for the
intersection of finitely many type classes, and the empty intersection {}
is the "top" or "full" sort (not the empty sort).
Makarius
Last updated: Apr 25 2024 at 12:23 UTC