*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] What are the atomic terms in Isabelle/HOL?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 04 Jun 2012 07:43:21 +0200*In-reply-to*: <4FCC2AE7.5020405@gmx.com>*References*: <4FCC2AE7.5020405@gmx.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1

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

**Follow-Ups**:**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*gottfried . barrow

**References**:**[isabelle] What are the atomic terms in Isabelle/HOL?***From:*gottfried . barrow

- Previous by Date: Re: [isabelle] proof dags?
- Next by Date: Re: [isabelle] proof dags?
- Previous by Thread: [isabelle] What are the atomic terms in Isabelle/HOL?
- Next by Thread: Re: [isabelle] What are the atomic terms in Isabelle/HOL?
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list