*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] What are the atomic terms in Isabelle/HOL?*From*: gottfried.barrow at gmx.com*Date*: Mon, 04 Jun 2012 14:07:33 -0500*In-reply-to*: <CAMej=24=CZSjwg5sUz9OnVTT31qagw5H6BBErsh3N7kPoOh3mg@mail.gmail.com>*References*: <4FCC2AE7.5020405@gmx.com> <4FCC4AF9.1060304@in.tum.de> <4FCCB56F.6040403@gmx.com> <CAMej=24=CZSjwg5sUz9OnVTT31qagw5H6BBErsh3N7kPoOh3mg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Ramana,

http://hol.sourceforge.net/documentation.html

Two books I would add to my previous list are these: "The HOL System LOGIC", HOL4 Documentation http://hol.sourceforge.net/documentation.html "Logic and Computation: Interactive Proof with Cambridge LCF", by Lawrence Paulson (Amazon) Thanks for the clarifications. --GB On 6/4/2012 10:54 AM, Ramana Kumar wrote:

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 ofLCF, MLor Haskell. The document Programming and Proving in Isabelle is anintroductionto 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 ofwhat aterm is: Terms may also contain lambda-abstractions. I've looked for other definitions of "term" in the Isabelle docs, butI'm notsure how constants and variables are used as a part of the definitionof "term".Here are three questions I've asked myself, with my answers inparentheses. Youcan 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 relatedto constants.I briefly looked at "3.2.5 Types and terms" in isar-ref.pdf, but Ican't sortthat 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 CambridgeLCF", 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/HOLterms maynot be limited to function application, but I tend to take thingsliterally, sowhen prog-prove.pdf says, "Terms are formed as in functionalprogramming byapplying functions to arguments", that makes me wonder whether a termis onlyfunction 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" ofPaulson's "Logicand Computation" apply to Isabelle/HOL? Part I chapters 2, 3, and 4 of "Logic and Computation" look likesomething Ineed to work through for foundational material on HOL. Thanks, GB

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

**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*Tobias Nipkow

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

**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] What are the atomic terms in Isabelle/HOL?
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [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