[Prev][Next][Index][Thread]
Map theory--addendum
Return-Path: <grue@rimfaxe.diku.dk>
Date: Tue, 8 Sep 92 15:54:52 +0200
...
In addition, and contrary to set theory, map theory has
unlimited abstraction and contains a computer programming
language as a natural subset.
Klaus Grue
Presumably these terms must be defined carefully in order to prevent
SETL from being a "natural subset" of set theory.
Vaughan Pratt
Here is a more complete (and longer) description:
Map theory has six basic concepts: Functional application,
lambda abstraction, if-then-else, a single atom T, Hilbert's
epsilon operator (also known as the choice operator) and a
'well-foundedness' predicate. Omitting Hilbert's epsilon
operator and the well-foundedness predicate yields a Turing
complete computer programming language.
On the contrary, ZFC has four basic concepts: Membership, negation,
implication and universal quantification. No subset of these
concepts form a Turing complete computer programming language.
ZFC has limited abstraction in that {x|p(x)} merely is guaranteed
to exist if x is restricted to some set.
Map theory has unlimited abstraction in the sense that for any
expression E(x), the map f = \x.E(x) satisfies f(x) = E(x) for
all x. Among other, the expression E can contain existential and
universal ZFC quantifiers (which are defined on basis of Hilbert's
epsilon operator).
As an example, map theory allows the fixed point operator to be
applied to the universal quantifier of ZFC. That is impossible
in ZFC because the fixed point operator is not definable; it is
impossible in SETL because SETL does not have the universal
quantifier of ZFC. The example is not particularly useful since
the fixed point operator applied to the universal quantifier
yields 'bottom'.
Klaus Grue