Re: Types and sorts

William M. Farmer (farmer@linus.mitre.org)
Thu, 25 Aug 1994 10:18:30 -0400

The purpose of my previous note was to point out the distinction
between "types" with syntactically based operator/arguments checking
and "sorts" with semantically based operator/arguments checking. I
did not intend the note to be a presentation of the IMPS logic. I
have listed at the end of this message two references for those who
might be interested in looking at the details of how partial functions
and sorts are handled in the IMPS logic.

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 = ""
}