*To*: gottfried.barrow at gmx.com*Subject*: Re: [isabelle] What are the atomic terms in Isabelle/HOL?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Mon, 4 Jun 2012 16:54:17 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FCCB56F.6040403@gmx.com>*References*: <4FCC2AE7.5020405@gmx.com> <4FCC4AF9.1060304@in.tum.de> <4FCCB56F.6040403@gmx.com>*Sender*: ramana.kumar at gmail.com

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

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

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

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

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

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