# [isabelle] What are the atomic terms in Isabelle/HOL?

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*