Sorts
Sorts are heavily used in Leibniz to categorize and describe terms, but also to check for elementary mistakes such as adding a number and a character string.
A sort describes a set of terms. The set is defined by the operators that have the sort as its value sort.
To make it easier to distinguish sort names from operator names, sort names are shown in italics.
Sorts can be organized in
sort hierarchies
via
subsort declarations
. If sort a
is declared to be a subsort of sort b
, then all terms of sort a
are also terms of sort b
. Put differently, the set described by a
is a subset of the set described by b
. Subset declarations define a
partial order
on sorts, which is described by a
directed acyclic graph
.
For an example of a subsort graph, see the sort graph of the context Integers:
(LzGlobalCache uniqueInstance contextFor: 'Integers') sortGraph
For a more complex example, see the sort graph of the context Real numbers:
(LzGlobalCache uniqueInstance contextFor: 'Real numbers') sortGraph
The sort graphs for integers and real numbers each consist of two distinct groups that are not connected via subsort relations, i.e. the graphs each have two connected components . The connected components of a sort graph are called kinds . A kind is printed as a list of sorts in square brackets, the sorts being the maximal sorts of the kinds, i.e. the sorts that are not subsorts of any other sort. You can click on the kind names in the sort graph to get an enlarged view of just one kind, and in that graph you can then click on each sort to learn more about it.