Email Gateway (Aug 18 2022 at 20:11): Email Gateway (Aug 18 2022 at 20:11):From: gottfried.barrow@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
Email Gateway (Aug 18 2022 at 20:12):From: Makarius <makarius@sketis.net>
On Mon, 4 Jun 2012, Ramana Kumar wrote:
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.
Yes, this is basically all the same for Isabelle, although the HOL-ish
colon is not part of the name of types in Isabelle; instead double colon
is used as mere notation.
I often use myself the terminology "type constructor" and "type constant"
interchangeably, although it might confuse beginners -- who are already
confused by the idea of term constant with functional types.
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.
A little, but not much. Type classes are just predicates over types plus
some sophisticated extra-logical infrastructure to make it all fit
together, including qualified type inference in the style of Haskell98 and
code-generation.
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").
Yes, the Isabelle/Pure framework clearly distinguishes 3 main categories
of types, terms, theorems --- so these are apples, pears, peaches.
See also
http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf
especially chapter 2, where all this is presented in a condensed manner,
with references to the corresponding ML functions. Section 2.3.2 is
particularly funny: it shows some tricks to mix the different kinds of
formal fruit.
Makarius
Email Gateway (Aug 18 2022 at 20:14):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 20:20):From: gottfried.barrow@gmx.com
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
Email Gateway (Aug 18 2022 at 20:20):From: Ramana Kumar <rk436@cam.ac.uk>
On Mon, Jun 4, 2012 at 2:17 PM, <gottfried.barrow@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,
GBOn 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@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
Email Gateway (Aug 18 2022 at 20:20):From: gottfried.barrow@gmx.com
Ramana,
Your HOL4-centric clarification of "types" and "terms" reminded me of
your suggestion to Bill, in the thread "rigorous axiomatic geometry...",
that he should look at the HOL4 document titled "The HOL System Logic".
http://hol.sourceforge.net/documentation.html
I've had the main HOL4 manuals on my hard drive for months, but I forgot
about using them as a general source of information on HOL.
The three BNF grammars for "types" and "terms" on pages 10 and 15 also
fall under the "Dude, this is awesome" category, along with your
clarifications, and the detailed explanations in the manual, which I'll
eventually study.
Collectively, the Isabelle docs, HOL4 docs, and related textbooks are
awesome. A lot of theorem assistants don't have enough documentation to
get people over the barrier to entry.
Still, because the books are spread around that give a foundational
understanding of what Isabelle/HOL is, it can make it hard to know where
to start. But that's other people's problem. I think I have a basic grip
on what it is now, and how to learn about it. And in understanding
Isabelle/HOL, I should get an understanding of how to reinvent whatever
object-language-wheel I want to on top of it.
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
Email Gateway (Aug 18 2022 at 20:22):From: gottfried.barrow@gmx.com
On 6/4/2012 10:54 AM, Ramana Kumar wrote:
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)....
Base types, type constructors, and function types are all kinds of type
constants, or can be viewed as such....
A function type could be thought of a type constant for functions with
arity 2 (taking the domain and range types as arguments).
Yea, you're right. Not surprising. And TUM PhD theses are good for
clarifying the Isabelle terminology.
Types tau are either type variables alpha or applications of type
constructors k^n with fixed arity n...
"Proving Theorems of Higher-Order Logic with SMT Solvers", page 4
http://www21.in.tum.de/~boehmes/phd_thesis.html
So the atomic types are type variables and type constructors of arity 0.
I guess.
The HOL4 terminology in the HOL4 logic manual is not the perfect goto
document for explaining the Isabelle termininology.
I'm not sure what "type constructors" refers to, but probably it's just a
synonym for type constants.
It turns out that it's the opposite, that "type constants" is a synonym
for "type constructors". Synonyms being what they are, that's not a
problem.
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.
The list doesn't appear to be overly concerned with enforcing correct
word usage. Lists are busy sometimes.
--GB
Last updated: Apr 25 2024 at 20:15 UTC