[Prev][Next][Index][Thread]
second reply to Scott Finnie
Further comparisons of types and sets
I agree with most of what Robin Adams said, indeed I considered
before ending my first reply to Scott Finnie whether to talk about the
difference between the membership judgements of type theory, say a:A, and
the membership proposition, a in A, of set theory. This is one of the
most difficult points for people to understand who approach type theory
from mathematics, logic and set theory. The issue can be treated
naturally in logic if one considers typed logic as distinct from
multi-sorted predicate logic.
In typed logic, the quantifiers have the form All x:A.B and Some x:A.B.
The rule for existential introduction looks roughly like this
H |- B[a/x] H |- a:A
----------------------------
H |- Some x:A.B
The sequent form H |- a:A is telling us the type of object a, and the
conclusion is not a proposition, but in the terminology of Martin-Lof and
Frege, it is a judgement. It does not make sense to negate this judgement
since it is telling us what a is. We are saying " a is_an A", for
example, 0 is_a Nat. It is not sensible to deny this judgement because
it is simply declaring what 0 is. We see this in natural discourse when
we declare something like "I am here now" or "this is zero".
The elimination rule for existentials also reveals the use of typing
judgements (or declarations) among hypotheses as follows.
H, x:A, B |- G
-----------------------
H, Some x:A.B |- G
In this case, the typing judgement occurs among the hypotheses, and we can
think of it as a "declaration" about x. So in a sequent style
presentation of the proof rules of typed logic, we expect to see
declarations as well as propositions on the left hand side.
Martin-Lof type theory can make finer distinctions than ZF set theory, it
can reason about whether an expression is meaningful. For example,
proving exp:Nat is telling us that exp is a meaningful expression denoting
a natural number. Proving P:Prop is telling us that P is a meaningful
expression for a proposition. Such judgements come up in trying to prove
something like Some x:Nat. (5/x = 0). It is informative to ask whether
this is a meaningful proposition. We cannot take 0 for x because we
cannot prove that 5/0:Nat, indeed 5/0 is meaningless in Martin-Lof style
type theories. (For a really subtle point, one might want to see that in
a type theory like Nuprl, the Y-combinator can be typed so it is possible
to write partial recursive functions, say f, and then f(x):A tells us that
the function terminates on input x.)
I am about to finish an article that approaches type theory from the point
of view of set theory, it is called Naive Computational Type Theory, and
it will be on the Web for awhile in about ten days at the Nuprl home page
that I mentioned before. In due course, my colleague Stuart Allen will
also post an article which discusses the philosophical foundations of type
theory starting from Russell's notion that a type is the domain of a
function. He provides some new philosophical justifications.
The beauty of type theory is that it sheds new light on issues in computer
science, mathematics, logic, philosophy and linguistics (see the work of
Aarne Ranta). In all spheres the results are quite profound. For example,
some proof theorists now believe that the results of Michael Rathjen on
the consistency of fragments of analysis relative to Martin-Lof type
theory have re-opened Hilbert's program. In computer science the research
program of TAL, typed assembly language, started by Greg Morrisett is a
promising way to achieve much higher confidence in mobile code. Also the
ideas of Bob Harper and Karl Crary for using type theory to provide the
semantics of programming languages is a major topic in languages and
systems. These explorations in computer science are ultimately based in
type theory and they are generating many exciting new research questions
about types, and providing more evidence that type theory is the right
foundational language for computer science as well as for computational
mathematics.
Bob Constable