Re: [isabelle] What are the atomic terms in Isabelle/HOL?



On Mon, 4 Jun 2012, Ramana Kumar wrote:

Base types, type constructors, and function types are all kinds of type
constants, or can be viewed as such.
A base type might be ":bool", the type of propositions, which may be
considered as the type constant "bool" applied to no arguments.
(Indeed, every type constant has a fixed number, its arity, of arguments it
ought to take.)
A function type could be thought of a type constant for functions with
arity 2 (taking the domain and range types as arguments).
I'm not sure what "type constructors" refers to, but probably it's just a
synonym for type constants.
If I'm getting some details of Isabelle wrong here, I'm sure the list will
point it out. I'm speaking primarily from my knowledge of HOL.

Yes, this is basically all the same for Isabelle, although the HOL-ish colon is not part of the name of types in Isabelle; instead double colon is used as mere notation.

I often use myself the terminology "type constructor" and "type constant" interchangeably, although it might confuse beginners -- who are already confused by the idea of term constant with functional types.


I know Isabelle also has type classes, which complicates the story a bit,
but you haven't mentioned them so I won't say anything further.

A little, but not much. Type classes are just predicates over types plus some sophisticated extra-logical infrastructure to make it all fit together, including qualified type inference in the style of Haskell98 and code-generation.


By all this it now seems clear to me that atomic types are distinct from
atomic terms.

Indeed all types, atomic or not, are distinct from all terms, atomic or
not, in higher-order logic (or "simple type theory").

Yes, the Isabelle/Pure framework clearly distinguishes 3 main categories of types, terms, theorems --- so these are apples, pears, peaches.

See also http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf especially chapter 2, where all this is presented in a condensed manner, with references to the corresponding ML functions. Section 2.3.2 is particularly funny: it shows some tricks to mix the different kinds of formal fruit.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.