Doug Hoover says:
> farmer@linus.mitre.org writes:
>
> There is a distinction between "types" and "sorts" in the IMPS logic
> (officially named LUTINS) that might be helpful to the recent
> discussion about type theory vs. set theory.
>
> etc.
>
> I wonder if he would be willing to compare the type theory of IMPS to
> that of PVS. In PVS, types are closed under subtypes (any predicate
> defines a subtype of a type) so it appears that
>
> PVS-type = IMPS-(type or sort)
>
> I prefer PVS because I don't see the advantage of distinguishing types
> and sorts. Am I missing something?
First, IMPS types are implemented as special kinds of sorts: a type is
just a maximal sort, i.e., a sort which is not a proper subsort of any
other sort. Every sort s is a subsort of a unique type t. The types
are used (exactly as in Church's system) to determined whether
expressions are well-formed, but otherwise they are used just like
other sorts.
The type system of PVS is, in spirit, very similar to the sort system
of IMPS. PVS types are used in much the same way as IMPS sorts, and
type checking in PVS, which is semantically based, is much like
definedness checking in IMPS. However, partial functions are handled
differently in the two systems. In PVS a partial function from, say,
the integers to the integers with domain D is formalized as a total
function with type d->i where i is the type of integers and d is a
subtype of i that denotes D. I think the approach in IMPS is more
flexible since it is not necessary to always declare or construct a
type corresponding to the domain of the partial function.
Bill Farmer
===========================================================================
@Article{Farmer90,
author = "W. M. Farmer",
title = "A Partial Functions Version of {Church's} Simple
Theory of Types",
journal = "Journal of Symbolic Logic",
year = "1990",
volume = "55",
Optnumber = "3",
pages = "1269-91",
OPTmonth = "",
OPTnote = "Also {\sc mitre} Corporation technical report M88-52,
1988; revised 1990."
}
@Article{Farmer93b,
author = "W. M. Farmer",
title = "A Simple Type Theory with Partial Functions and Subtypes",
journal = "Annals of Pure and Applied Logic",
year = "1993",
volume = "64",
OPTnumber = "3",
pages = "211--240",
OPTmonth = "",
OPTnote = ""
}