Re: [isabelle] What are the atomic terms in Isabelle/HOL?
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and