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



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, though there might not be such a thing as a "type constant". 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".

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.

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.