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



On Mon, Jun 4, 2012 at 2:17 PM, <gottfried.barrow at gmx.com> wrote:

> Tobias,
>
> Thanks. I'm trying to get the vocabulary down.
>
> Unless you tell me different, I'll conclude that term constants and term
> variables are different than type constants and type variables,


Correct.


> though there might not be such a thing as a "type constant".


No, there are type constants. They are also known as "type operators".
Every type is either a type variable or a type constant applied to a list
of argument types (the list may be empty).


> I see (morely clearly now) that you did precede the introduction of
> "terms" with introducing "base types", "type constructors", "function
> types", and "type variables", though I see no "type constant".
>

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.
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.


>
> The standard lambda-term definition is straight forward enough, but the
> type definition is a little more slippery. Hindley's "Basic Simple Type
> Theory" says:
>
>   2A1 Definition (Types): An infinite sequence of type-variables is
>     assumed to be given, distinct from term-variables. Types are...
>     (i) each type-variable is a type (called an atom)
>
> Somehow, "distinct from term-variables" escaped my attention. Still,
> there's only mention of type variables. I should have also looked at
> Hindley's "Lambda-Calculus and Combinators":
>
>   Definition 10.1 (Simple types): Assume we have a finite or infinite
>     sequence of symbols called atomic types; then...
>     (a) every atomic type is a type;
>
> "Atomic type" is sufficiently vague to allow for "type constants", and all
> sorts of other atomic types.
>
> 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").
There are other type theories where this is not true, but again you haven't
mentioned them so I'll shut up :)
By my reckoning "atomic types" should just be type variables, and possibly
also the type constants with arity 0.


>
> Thanks,
> GB
>
>
> On 6/4/2012 12:43 AM, Tobias Nipkow wrote:
> > Isabelle's terms are lambda-terms with a type system similar to that of
> LCF, ML
> > or Haskell. The document Programming and Proving in Isabelle is an
> introduction
> > to Isabelle, not a definition. Just like most textbooks on functional
> > programming it does not start out with the lambda-calculus on page 1.
> >
> > To answer the question in your title: variables and constants.
> >
> > Tobias
> >
> > Am 04/06/2012 05:26, schrieb gottfried.barrow at gmx.com:
> >> I'm looking at this sentence in prog-prove.pdf, page 3:
> >>
> >>      Terms are formed as in functional programming by applying
> >>      functions to arguments. If f is a function of type
> >>      tau1 =>  tau2 and t is a term of type tau1, then f t
> >>      is a term of type tau2.
> >>
> >> Also, the word "contain" in this sentence on page 4 makes me unsure of
> what a
> >> term is:
> >>
> >>      Terms may also contain lambda-abstractions.
> >>
> >> I've looked for other definitions of "term" in the Isabelle docs, but
> I'm not
> >> sure how constants and variables are used as a part of the definition
> of "term".
> >>
> >> Here are three questions I've asked myself, with my answers in
> parentheses. You
> >> can correct them if you'd like:
> >>
> >> 1) Does a term (of Isabelle/HOL) have a type?  (obviously yes)
> >> 2) Is a term (of Isabelle/HOL) a type? (no)
> >> 3) Is a type (of Isabelle/HOL) a term? (no)
> >>
> >> I'm guessing that one difference between a term and a type is related
> to constants.
> >>
> >> I briefly looked at "3.2.5 Types and terms" in isar-ref.pdf, but I
> can't sort
> >> that out.
> >>
> >> In intro.pdf (Old Introduction to Isabelle), page 1, it says:
> >>
> >>    The syntax for terms is summarised below...
> >>      t :: tau       type constraint, on a term or bound variable
> >>      %x . t         abstraction
> >>      %x1...xn . t   curried abstraction, %x1...%xn . t
> >>      t(u)           application
> >>      t(u1,...,un)   curried application, t(u1) ... (un)
> >>
> >> This indicates that a lambda-abstraction can be a term.
> >>
> >> In Paulson's "Logic and Computation - Interactive proof with Cambridge
> LCF", in
> >> "Chapter 5 Syntactic Operations for PP-Lambda", page 142, he says:
> >>
> >>      Terms come in four syntactic classes: constants, variables,
> >>      abstractions, and combinations (function applications).
> >>
> >> This is like a lambda-calculus term, so it looks as if Isabelle/HOL
> terms may
> >> not be limited to function application, but I tend to take things
> literally, so
> >> when prog-prove.pdf says, "Terms are formed as in functional
> programming by
> >> applying functions to arguments", that makes me wonder whether a term
> is only
> >> function application.
> >>
> >> I'll ask two more questions, in case someone wants to answer them:
> >>
> >> 1) Is a term (in Isabelle/HOL) function application only? (probably not)
> >> 2) To what extent do the concepts in "Part II Cambridge LCF" of
> Paulson's "Logic
> >> and Computation" apply to Isabelle/HOL?
> >>
> >> Part I chapters 2, 3, and 4 of "Logic and Computation" look like
> something I
> >> need to work through for foundational material on HOL.
> >>
> >> Thanks,
> >> GB
> >
> >
>
>
>
>




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