[Indigo]<KRL>document>rep-quant!2

Page Numbers: Yes First Page: 1
Heading:

June 16, 1977 11:19 AM [IVY]<KRL>document>rep-quant

Status: This is the form designed for the ultimate KRL-1 document. It therefore is a mixture of philosophy, specification, etc. The specifications are wrong in one important way -- their treatment of quoted forms is out of line with our current notions, which emphasize protyotypes instead. I will get in and fix this up, but in the meantime, the general outline stands, and the detailed functional and unit names are more or less right. All of the lambda stuff will also go away, through the use of unit constructors (see <KRL>unit.doc)

Listing of the current specification documents for KRL-1

Contents

A. Overview of what is in the system

B. The level 1 representations

C. The level 3 forms for collection enumeration

1. The basic forms (including ellipsis)

2. The meaning of reflexives in enumeration descriptions

D. The fundamental units for dealing with collections

1. Sets

2. Orderings

3. Sequences

4. Mathematical mappings

E. Forms for giving descriptions applicable to members or sets of members of collections

1. Lambda forms

2. Forms for describing set mapping relationships

F. Changing Collections

!!!!!!!!!!!!!!!!!!!!!!!

G. Units for Arithmetic -- this belongs elsewhere but is here temporarily

Units and functionals for collections (Sets and Sequences) -- this belongs in the section on Standard Units but is here temporarily

!!!!!!!!!!!!!!!!!!!!!!!

The state of this file: It is still very incomplete. Sections on the level 1 semantics and on the descriptor forms are totally left out, and the section on Changing Collections is sketchy at best. The set of units and functionals are a proposal, and at the moment what is important is the set of names and basic meanings. The exact details of how things are defined (e.g. sequences in terms of mappings from the integers) can be argued out later. The listing at the end (which will go into the chapter of standard units) is alphabetical. The index which precedes it includes functional names as well, in their appropriate alphabetical place. There is nothing written yet on how the system will make use of descriptions involving sets and sequences. That will eventually get written into the sections on the interpreter, access compiler, etc.

!!!!!!!!!!!!!!!!!!!!!!!

8A. Overview of what is in the system

With sets, orderings and sequences, as with worlds, KRL-1 includes an extra layer of structuring beyond that provided by the bare notational mechanisms of KRL-0. The additional mechanism can be described in terms of a set of units, functionals, and standard descriptions for these objects. However, this mechanism is something more than a "package" provided to users, since its conventions are built into the interpreter and compiler. The major facilities provided are:

* A set of notations

* Set and sequence enumeration descriptors

* Units for Set, Ordering and Sequence with associated functionals, such as Union, Intersection, MemberOf, SubsetOf, etc.

* Units and functionals for associating collections with descriptions of their elements, such as SetOf, MapSet, MapSequence, SetOfAll, SequenceOfAll, etc.

* Specialized forms for the basic description operations

* Forms to produce values which are sets and sequences

* Operations to modify descriptons by adding and removing set members

* The recognition of set and sequence descriptions in initial descriptions provided to the basic description operations, and their use in a "generate and test" mode

* Inference rules about set and sequence structure built into the interpreter

* Specialized versions of mechanisms for describing changing beliefs in a temporal world structure, when those changes represent alterations to the membership of a set or sequence

8B. The level 1 Representations

This still needs to be written (and designed)

8C. The level 3 forms for collection enumeration

8C1. The basic forms (including ellipsis)

8C2. The meaning of reflexives in enumeration descriptions

8D. The fundamental units for dealing with collections

8D1. Sets

The units for sets are based on primitive notions of Set, cardinality and SetMembership. They are not defined anywhere in the declarative part of the system, but are recognized by the interpreter which has procedures for drawing appropriate inferences. There has been no attempt to reduce this to a minimal axiomatization of set theory, and there are many ways in which reductions would be possible. This is not important for the KRL interpreter (or user), since reasoning proceeds on the basis of having knowledge about the higher level constructs, rather than always working from primitive notions and axioms. For a general discussion of the attitude towards formal reduction in KRL, see Section ?? In reading the units given in this chapter, it is important to keep in mind that the descriptions are not intended as formal definitions, etither in the precise mathematical sense, or as a basis for the running of the interpreter. They are simply a useful set of cross-linkages and conceptual connections between the different units defined.

The following units are reduced versions of the actual ones (which appear in Appendix D), leaving out descriptions whose content will be explained later.

# Set
cardinality: A CardinalNumber

# SetMembership
set: A Set
element: A Thing

There is an important design decision implicit in these definitions:

* A Set is not its members: Set equality is a relationship between two distinct sets, stating that they have all the same members. Thus, the sets "The set of all even primes" and "The set of all divisors of 1024" can be distinct (non-coreferential) entities even if there is a mapping of Set equality which holds between them.

There is a functional MemberOf which takes a collection (sequence, ordering or set) as its argument and is used to describe an element of that set. It could have been defined on the unit for SetMembership, using: HasFunctional(element, MemberOf, set) but is instead defined in a more general CollectionMembership unit so that it can apply to orderings and sequences as well. The functional HasMember is the inverse of MemberOf

In addition to being able to associate elements with a Set, it is useful to associate descriptions of the elements. There are two basic forms, one for a description which is necessary for set membership (i.e. it describes all of the members), and one for a description which is both necessary and sufficient (i.e. anything fitting the description is a member). Formally:

# SetElementDescription↑11: HasFunctional(set, SetOf, quoted description)
set: A Set
description: A DescriptionForm
Which↑2 Describes(MemberOf↑3(My set))
2: ForAll(Noteref 3)

# SetElementSufficientDescription↑11: HasFunctional(set, SetOfAll, quoted description)
set: A Set; SetOf(My description)
description: A DescriptionForm
Not(Which Describes (Not(MemberOf(My set)))

The first unit uses the notation for quantifiers (See section ??) to indicate that for every thing described by MemberOf(My set) there is a relation of Describes between the description form and the thing. The descriptor SetOf(An Integer) is applicable to any set containing integers, while SetOfAll(An Integer) is precisely the set of all integers. It is possible to have sets represented in the system (i.e. have entities for them) for which no description of the members (sufficient or necessary) is known. The description form which fills the description slot in instances of these units is a standard Level 3 object.

There are standard units and functionals for Subset, Intersection, Union, SetDifference, and Partitions. See Appendix D for the details.

8D2. Orderings

An Ordering is made up of a Set, along with a set of order relation pairs. The basic units (reduced form to show only the descriptions relevant here) are:

# Ordering
elements: A Set
relation: An OrderingRelation
pairs: SetOf(An OrderPair with
ordering = My self
top = MemberOf(My elements)
bottom = MemberOf(My elements))

# OrderPair↑11: HasFunctional(top, Follows, bottom, ordering)
HasFunctional(bottom, Precedes, top, ordering)
HasFunctional(top, SuccessorOf, bottom, ordering)
HasFunctional(bottom, PredecessorOf, top, ordering)
self: <My bottom, My top>
top: MemberOf(The elements from My ordering)
bottom: MemberOf(The elements from My ordering)
ordering: An Ordering

ElementOfOrdering↑1
1: HasFunctional(MemberOf immediateFollowers, NextAfter, self, ordering)
HasFunctional(MemberOf immediatePredecessors, NextBefore, self, ordering)
self: MemberOf(The elements from My ordering)
immediateFollowers:
SetOfAll(MemberOf(The elements from My ordering)
SuccessorOf (My self, My ordering)
Not(SuccessorOf (SucessorOf (My self, My ordering),
My ordering)))
immediatePredecessors:
SetOfAll(MemberOf(The elements from My ordering)
PredecessorOf (My self, My ordering)
Not(PredecessorOf (PredecessorOf (My self, My ordering),
My ordering)))
ordering: An Ordering

Several points are noteworthy:

* An Ordering is not the set of its elements: The elements slot is not a self slot. There could in fact be several different orderings all having the same set of elements.

* An Ordering is not the set of order relationship pairs: Although it would be mathematically possible to define it this way. The pairs form one of the pieces of information about an ordering.

* A Sequence enumeration descriptor can be used to specify individual order pairs: The description <My bottom, My top> appearing in the self slot of an OrderPair indicates that a sequence descriptor which lists two elements is a valid description of an order pair. Thus, an order in which A precedes B can be described as (equivalently):

An Ordering with pairs = HasMember(<A,B>)
An Ordering with pairs = HasMember(An OrderPair with bottom = A top = B)

* The pairs associated with an ordering are all of the valid order pairs, not just the set of immmediately adjacent elements, and not a set associated with partial knowledge: An ordering is a mathematical object, and partial representations of it must be explicitly marked as such. Orderings are transitive (although this is not reflected in the descriptive form as written above -- in a complete representation, it would be). Thus, for example the following description is inconsistent since it uses a complete enumeration descriptor, but gives a set of pairs for which transitivity does not hold: An Ordering with pairs = {<1,3>,<3,5>}. A correct description would use the incomplete enumeration form, and might be: An Ordering with pairs = {<1,3>,<3,5> ...}. To specify that the ordering contains only those pairs derivable from a set, it is necessary to use the TransitiveClosure unit

* The orderRelation is not used directly: The unit for Ordering has a slot for a relation, but does not specify systematically how mappings which involve that relation are connected to the pairs in the ordering. It is possible to define such connections for particular relations (Maybe there will be a systematic notation -- how imporant is it?) Note that procedural attachments for dealing with specific order relations can be associated with the appearance of that relation in an instance of Ordering

8D3. Sequences

A Sequence is fundamentally different from an ordering in that an element can appear at more than one place within it. It is impossible to have an ordering in which A both follows and precedes B, but is is perfectly allright to have a sequence describable as <A, B, A, B, ...>. There is a correspondence between total orderings and non-redundant sequences, and some of the functionals are defined using units which take advantage of this correspondence. However as a means of convenient description, sequences are defined as mappings (in the mathematical sense) from the integers Note: there will probably be a primitive level 1 notion of sequence which is not defined in terms of mappings onto the integers, but the same set of unit and funcitonal names will be applicable in writing descriptions involving sequences:

# Sequence
length: A CardinalNumber; The cardinality from My pairs
pairs: MapSet(IntegerInterval(1, My length),
Lambda(’Integer,
\A SequencePositionPair with
sequence = My self
position = That(Integer))
elements: SetOfAll(The element from a SequencePositionPair
thatIs MemberOf(My pairs))

# SequencePositionPair↑11: HasFunctional(element, Nth, position, sequence)
HasFunctional(sequence, HasNth, position, element)
self: <My position, My element>
element: A Thing
sequence: A Sequence
position: An Integer
MemberOf(IntegerInterval(1,The length from My sequence))

Several new notations are used in these definitions. They will be explained below. There are standard functionals for SubSequence, SequenceConcatenation, and FrontElement and BackElement. see Appendix D.

8D4. Mathematical mappings

The word "mathematical" is used whenever it is necessary to distinguish between the notion of mapping as used in KRL, and its use in mathematics to represent a set of ordered pairs of elements.

# MathematicalMapping
pairs: SetOf(A MathematicalMappingPair with mapping = My self)
range: SetOfAll(The rangeElement from a MathematicalMappingPair
thatIs MemberOf(My pairs))
domain: SetOfAll(The domainElement from a MathematicalMappingPair
thatIs MemberOf(My pairs))

# MathematicalMappingPair
self: <My domainElement, My rangeElment>
mapping: A MathematicalMapping
rangeElement: MemberOf(The range from My mapping)
domainElement: MemberOf(The domain from My mapping)

# OneOneMap↑11:FurtherSpecified(MathematicalMapping)
range: A Set with cardinality = The cardinality from My domain

8E. Forms for giving descriptions applicable to members or sets of members of collections

In the basic units given above, the unit SetElementDescription and the associated functional SetOf provided a mechanism for giving a description which applied to each element of a set. There are two related extensions of this idea: describing arbitrary combinations of elements of different kinds of collections; and having a naming convention for referring to the elements being described. We will discuss these in reverse order, taking the simple case first, in which a single element is being described.

8E1. Lambda forms

Assume we want to describe the set of all people who shave themselves, and that there is a unit:

# Shave
shaver: A Person
shavee: A Person

The form SetOfAll(The shaver from a Shave) defines the set of all the people who shave anyone. The form SetOfAll(The shaver from a Shave; The shavee from a Shave) describes anyone who both shaves and is shaved, but there is no indication that he or she is the shaver and shavee in a single shaving. One solution is to create a new unit:

# SelfShaver
self: A Person
The shaver from a Shave with shavee = My self

We could then simply use SetOfAll(A SelfShaver). The My self descriptor is not appropriate unless this unit is created, since it would refer to the instance of the entire unit in which the SetOfAll descriptor appeared, not to the specific element of the set. However, this violates the spirit of KRL in that the division of knowledge into units is supposed to be used to control memory access. A user should not be forced into creating a new concept (a SelfShaver) just because there is no other way to express the self reference.

The solution we have taken is to provide a more general naming mechanism, based on the lambda calculus, using substitution in level 3 forms. The necessity for some such mechamism was made obvious by trying to deal with the cases of multiple-element descriptions below. The details of the particular mechanism we have chosen are determined by convenience, and are open to discussion. The basis is the notion of LambdaConversion which can be defined using the KRL meta-level units. The following is simply a skeleton which names the relevant participants:

# LambdaForm↑11: HasFunctional(self, Lambda, variable, form)
variable: Or(A LispAtom, SequenceOf(A LispAtom))
form: A DescriptionForm

# SingleLambdaConversion
lambdaForm: A LambdaForm with variable = A LispAtom
value: A Thing
convertedForm: A DescriptionForm

A Lambda form is a KRL level 3 object, but there is no special syntactic form to present one. The functional Lambda makes it possible to describe a LambdaForm. It is not a part of the KRL syntax, but is an ordinary functional which deals with level 3 objects as its referents. The convertedForm is a copy of the form from the lambdaForm in which every instance of a functional with functionalName = That and with its single argument a unit coreference descriptor with a variable from the LambdaForm as its Unit is replaced by a descriptor which has as its meaning a coreference with the corresponding element of the value. There are a number of subtle issues here, since there may be no labelled anchor for the value, and therefore no simple level three form which could be substituted. However, it seems that through appropriate use of meta-description, this could be handled (within a single activation context), and it is certainly the case that the interpreter can recognize and handle instances of this relationship specially, so that the result is consistent with the desired semantics.

This unit can be used in turn to define units which allow descriptions to be associated with elements of a Set:

# ReflexiveLambdaApplication↑11: HasFunctional(object, Satisfies, form)
object: A Thing
form: A LambdaForm
The lambdaForm from a SingleLambdaConversion with
value = My object
convertedForm = Which Describes My object

This unit involves the use of an object in two ways -- it is both the element substituted for the lambda variable, and the referent of the converted description. There are different uses of lambda application in which the value and the thing described by the resulting form are distinct, as described below.

Using the functionals defined above, we can define a set of people all of whom shave themselves:

SetOf(Satisfies (Lambda (’Shaver, \The shaver from a Shave with
shavee = That(Shaver))))

or the set of all people who shave themselves:

SetOfAll(Satisfies (Lambda (’Shaver, \The shaver from a Shave with
shavee = That(Shaver))))

The variable name is a dummy -- it is used only for substitutions, and those are done only when it appears as the argument to That. Other appearances of the same unit are left exactly as they appear in the form of the LambdaForm. The same functional is used in defining units for SetSelection and the functional ThoseIn which describe a subset by giving a set which contains it, and a description which fits only the selected members. We might have, for example, a definition of all those in the set of "good guys" who shave themselves:

Thosein(GoodGuys,
\(Satisfies (Lambda (’Shaver, \The shaver from a Shave with
shavee = That(Shaver))))

Note: The arguments to these functionals follow the standard interpretation of quoted forms as descriptions of level three forms. This includes the interpretation of reflexives according to a mapping whose prototype is the quoting context. Thus, the following unit has the intuitive (but hard to state in English) interpretation that "Any instance of barber has a corresponding set of customers, each of whom can be described as being shaved by that particular barber"

# Barber
customers: SetOf(The shavee from a Shave with shaver = My self)

This use of the reflexive My self is totally different from the use of a lambda to express that the noncustomers are each shaved by themselves:

# Barber
nonCustomers:
SetOf(Satisfies
(Lambda(’Person,
The shavee from a Shave with
shaver = That(Person))))

8E2. Forms for describing set mapping relationships

One of the standard ways of describing a set is by giving a domain set and a mapping function which is applicable to each element. In LISP, there are mapping functions (MAPCAR, MAPLIST, etc.) which express this relationship procedurally. In KRL, the description is declarative, rather than procedural -- it does not specify a specific sequence of operations to be carried out, but states a relationship. It is possible, for example, to specify that the set of perfect squares is the result of a mapping whose domain is the positive integers, and whose function is SQUARE. This description could then be used to generate random members of the set, without ever trying to compute all of them. The lambda mechanism described above is needed here, since a single range element is to be described in terms of a specific single domain element, but the description form as a whole is used as part of describing the set. The units are:

# LambdafiedPairDescription
pair: A MathematicalMappingPair
form: A LambdaForm
The lambdaForm from a SingleLambdaConversion with
value = The domainElement from My pair
convertedForm = Which Describes
The rangeElement from My Pair

# MapRangeDescription↑1
1: HasFunctional(range, MapSet, domain, form)
range: A Set
domain: A Set
form: A LambdaForm
mapping: A MathematicalMapping with
range = My range
domain = My domain
pairs =
SetOf(The pair from a LambdafiedPairDescription with
form = My form)

Thus, the set of all squares is:

MapSet(SetOfAll(An Integer),
Lambda(’Number, \Product(That(Number), That(Number))))

There is also a functional MapJoin which relates a domain to the union of all of its range elements (like the JOIN forms in CLISP), and corresponding mapping forms for sequences, MapSequence and JoinSequence, detailed in Appendix D.

Description of arbitrary subsets

Sets are often described by stating a relationship which holds between members. for example "A set of people, any two of whom have shaved each other". This could be done with nested lambda expressions, but this leads to awkwardness in preventing an element from being chosen repeatedly by the nested expressions. It is more natural to have a descriptor which is interpreted as: "Given any arbitrary set of n elements chosen from the set, the following holds". This is done using a notion of multiple variable lambda application:

# MultipleLambdaConversion
lambdaForm: A LambdaForm with variable = SequenceOf(A LispAtom)
value: SequenceOf(A Thing)
convertedForm: A DescriptionForm

# MultipleLambdaApplication↑1
1: HasFunctional(sequence, SequenceSatisfying, form)
sequence: SequenceOf(A Thing)
form: A LambdaForm with
variable = A Sequence with
length = the length from My sequence
The lambdaForm from a MultipleLambdaConversion with
value = My sequence
convertedForm = Which Describes My sequence

# ArbitrarySubsetDescription↑11: HasFunctional(set, EveryChoice, form)
set: A Set
form: A LambdaForm
subsetSize: An Integer
The length from a Sequence thatIs the variable from My form
sequences:
SetOfAll (A Sequence with
length = My subsetSize
elements = SubsetOf(My Set)
A Set with cardinality = My subsetSize)
SetOf (SequenceSatisfying(My form))

The example of a set every two of whom have shaved each other would be:

SetOf(A Person)
EveryChoice(Lambda(<’x,’y>,
\ Whose(’x, The shaver from a Shave with
shavee = That(y))))

The functional Whose plays a role complementary to That. In converting the lambda form, each occurence of Whose(var, description) can be thought of as being replaced by a description HasNth(n, description) which describes the sequence of values, and where n is the position of that variable name in the sequence of names which is the variable for the lambda form.

There are also forms for describing an arbitrary pair in an ordering, (EveryPair) an arbitrary adjacent pair in an ordering (EveryAdjacentPair), and an arbitrary adjacent subsequence of a sequence (EverySubsequence).

8F. Changing Collections

The units above are all static. In addition there are units for dealing with collections whose membership changes over time, but which are still regarded as a single conceptual entity. For example, "the set of living people over the age of 80" changes membership every instant, but is treated as a unified entity in all sorts of reasoning. The notion of "change" cannot be fully treated in KRL-1, since we have not formally dealt with process. However, there are a number of special cases which are useful, and for which standard units exist. These are supported to varying degrees by the interpreter. See Section ???? on worlds for more discussion.

# ChangingObject
description: A DescriptionForm
worlds: A WorldStructure; Usually(ProcessorTime)
history: The mapping from a MapRangeDescription with
domain = The contingentWorlds from My worlds,
form = Lambda(’World,
DescribedBy(My description)
with world = That(World)))
currentValue: DescribedBy(My description) with
world = CurrentWorld(My worlds)
operations: SetOf(An Operation)

There are lots of things hidden in this, and we are treading on thin water by handling the limited subset we can think of. However, the basic notions are:

* Mappings based on units whose prototypes are normal objects (e.g. sets) but whose instances are filled in with changing objects will be "type forced" to the current value when appropriate.

* There is a way of specifying the parameters for Describe to indicate that a current value is being changed. This includes the ability to state that something is being added to or removed from a set, etc. See Section 12.

* The access compiler will know about some standard units for describing changing collections which change in a systematic way, and will use this in deciding how to compile the special Describe actions. The operations slot is a way of documenting the names of these operations, but at the moment there is no systematic way of defining them. See Section 16

* The compaction scheme will make it possible for fields of compacted perspectives to be conceptually associated with changing collections, but with only the current value actually stored. See Section 16

For the moment, Appendix D contains only a skeleton set of units for standard changing collections, such as Queue, GrowingSet, Stack, etc. These need to be filled in with more formal definitions. It also contains a rough first cut at the process units, such as AddElement and RemoveElement. These also need to be filled out.

8G. Units for Arithmetic

These don’t really belong to the section on collections, but they are used here, so I am putting in a pointer to them. They will appear in a section labelled ARITHMETIC in the Standard Units of Appendix D. They haven’t been worked over much, so there are probably some obvious improvements possible.

# Addition↑11: HasFunctional(sum, Sum, set addends)
addends: SetOf(A Number)
sum: A Number

# CardinalNumber
self: Or([An Integer; A PositiveNumber], An Infinity)

# Integer↑11: Comment("This is probably primitive")
self: A Number

# Number↑11: Comment("This is probably primitive")
self: A Number

# NumericalOrder↑11: HasFunctional(greater, GreaterThan, lesser)
HasFunctional(lesser, LessThan, greater)
greater: A Number; Sum(My lesser, Or(0, a PositiveNumber))
lesser: A Number

# PositiveNumber
self: A Number; GreaterThan(0)

# Subtraction↑11: HasFunctional(difference, Difference, minuend, subtrahend)
minuend: Sum(My subtrahend, My difference)
subtrahend: A Number
difference: A Number

!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

Units and functionals for collections (Sets and Sequences)

AdjacentPair further specified OrderPair
(long, AddBack, item, short) in SequenceBackElement
(long, AddFront, item, short) in SequenceFrontElement
AdjacentPairDescriptionordering: form:
(difference, AllBut, element, set) in SetMembership
(short, AllButFirst, long) in SequenceFrontElement
(short, AllButLast, long) in SequenceBackElement
ArbitraryPairDescriptionordering: form:
ArbitrarySubsequenceDescriptionsequence: form: size: sequences:
ArbitrarySubsetDescriptionset: form: subsetSize: sequences:
(MemberOf minima, BottomElementOf, self) in Ordering
ChangingSequence
ChangingSet
CollectionMembershipcollection: element:
(fullSequence, Concatenation, sequence components) in SequenceConcatenation
(element, ElementOf, set) in SetMembership
ElementOfOrderingimmediateFollowers: immediatePredecessors: ordering
(ordering, EveryAdjacentPair, form) in ArbitraryPairDescription
(set, EveryChoice, form) in ArbitrarySubsetDescription
(ordering, EveryPair, form) in ArbitraryPairDescription
(sequence, EverySubSequence, form) in ArbitrarySubsequenceDescription
(finish, FinalSequenceOf, fullSequence) in SequenceConcatenation
(top, Follows, bottom, ordering) in OrderPair
GrowingSet
(collection, HasMember, element) in CollectionMembership
(sequence, HasNth, position, element) in SequencePositionPair
(start, InitialSequenceOf, fullSequence) in SequenceConcatenation
(sequence, IntegerInterval, bottom, top) in Interval
Intervalbottom: top: sequence:
(intersection, IntersectionOf, set components) in SetIntersection
(self, Lambda, variable, form) in LambdaForm
LambdafiedPairDescriptionpair: form:
LambdaFormvariable: form:
MapRangeDescriptionrange: domain: mapping: form:
(range, MapSequence, domain, form) in SequenceMapping
(range, MapSet, domain, form) in MapRangeDescription
MathematicalMappingrange: domain: pairs
MathematicalMappingPairmapping: rangeElement: domainElement:
(element, MemberOf, collection) in CollectionMembership
MultipleLambdaApplicationsequence: form:
MultipleLambdaConversionvalue: lambdaForm: convertedForm:
(MemberOf immediateFollowers, NextAfter, self, set) in ElementOfOrdering
MemberOf immediatePredecessors, NextBefore, self, set) in ElementOfOrdering
(element, Nth, position, sequence) in SequencePositionPair
OneOneMapFurtherSpecified MathematicalMapping
OrderedSetContainmentsubset: superset:
Orderingelements: pairs: relation: minima: maxima:
OrderingDescriptionsequence: description:
(ordering, OrderingOf, quoted description) in OrderingDescription
OrderingRelation
OrderPairtop: bottom: ordering:
PartitionFurtherSpecified SetUnion
(components, ParitionOf, union) in Partition
(bottom, Precedes, top, ordering) in OrderPair
(bottom, PredecessorOf, top, ordering) in OrderPair
Queue
ReflexiveLambdaApplicationobject: form:
(object, Satisfies, form) in ReflexiveLambdaApplication
(description, Selects, subset, superset) in SelectionDefinition
Sequencelength: pairs: elements:
SequenceBackElementitem: short: long:
SequenceConcatenationcomponents: start: finish: fullSequence
SequenceContainmentfirstPosition: lastPosition: subSequence: sequence: header:
SequenceDescriptionsequence: description:
SequenceEnumeration
SequenceFrontElementitem: short: long:
(rangeJoin, SequenceJoin, domain, form) in SequenceMapping
SequenceMappingdomain: range: rangeJoin: setMap: form:
(sequence, SequenceOf, quoted description) in SequenceDescription
SequencePositionPairelement: sequence: position:
(sequence, SequenceSatisfying, form) in MultipleLambdaApplication
Setcardinality:
SetContainmentsuperset: subset: difference
SetElementDescriptionset: description:
SetElementSufficientDescriptionset: description:
(difference, SetDifference, superset, subset) in SetContainment
SetEnumeration
SetIntersectioncomponents: intersection:
(set, SetOf, quoted description) in SetDescription
(set, SetOfAll, quoted description) in SetDefinition
SetMembershipelement: set: difference:
SetSelectionsuperset: subset: description
SetUnioncomponents: union:
SingleLambdaConversionlambdaForm: value: convertedForm:
Stack
(subset, SubOrderOf, superset) in OrderedSetContainment
(subSequence, SubSequenceOf, sequence) in SequenceContainment
(subset, SubsetOf, superset) in SetContainment
(top, SuccessorOf, bottom, set) in OrderPair
(superset, SuperOrderOf, subset) in OrderedSetContainment
(superset, SupersetOf, subset) in SetContainment
(object, That, variable) special functional used in Lambda forms
(subset, ThoseIn, superset, description) in SetSelection
(MemberOf maxima, TopElementOf, self) in Ordering
TotalOrderingsequence:
TransitiveClosuregiven: closure: ordering:
(union, UnionOf, set components) in SetUnion
(sequence, Whose, variable, description) special functional used in multiple lambda forms

# # # # # # # # # # # # # # #

# AdjacentPair↑11: FurtherSpecified(OrderPair)
top: NextAfter(My bottom, My ordering)

# AdjacentPairDescription↑1
1: HasFunctional(ordering, EveryAdjacentPair, form)
ordering: An Ordering with
pairs = SetOf(Implies(An AdjacentPair, DescribedBy(My form)))
form: A DescriptionForm

# ArbitraryPairDescription↑1
1: HasFunctional(ordering, EveryPair, form)
ordering: An Ordering with
pairs = SetOf(DescribedBy(My form))
form: A DescriptionForm

# ArbitrarySubsequenceDescription↑1
1: HasFunctional(sequence, EverySubSequence, form)
sequence: A Sequence
form: A LambdaForm with
variable = A Sequence with length = My size
size: An Integer
sequences:
SetOfAll (A Sequence with length = My size
MemberOf(The components from
A SequenceConcatenation with
fullSequence = My sequence))
SetOf (SequenceSatisfies(My form)))

# ChangingSequence
self: A ChangingObject with
description = \A Sequence
operations = SequenceOf(Or(An AddElementToSequence,
A RemoveElementFromSequence))

# ChangingSet
self: A ChangingObject with
description = \A Set
operations = SequenceOf(Or(An AddElementToSet,
A RemoveElementFromSet))

# CollectionMembership↑11: HasFunctional(element, MemberOf, collection)
HasFunctional(collection, HasMember, element)
collection: Or(A Set, An Ordering, A Sequence)
element: A Thing
Using My collection
A Set -> ElementOf(My collection)
An Ordering -> ElementOf(Its elements)
A Sequence -> ElementOf(Its elements)

# ElementOfOrdering↑1
1: HasFunctional(MemberOf immediateFollowers, NextAfter, self, ordering)
HasFunctional(MemberOf immediatePredecessors, NextBefore, self, ordering)
Comment("If the ordering slot is filled by a sequence, then it is interpreted
as the corresponding total ordering --(I’m not clear just how and
when this gets done)")
self: MemberOf(The elements from My ordering)
immediateFollowers:
SetOfAll(MemberOf(The elements from My ordering)
SuccessorOf (My self, My ordering)
Not(SuccessorOf (SucessorOf (My self, My ordering),
My ordering)))
immediatePredecessors:
SetOfAll(MemberOf(The elements from My ordering)
PredecessorOf (My self, My ordering)
Not(PredecessorOf (PredecessorOf (My self, My ordering),
My ordering)))
ordering: An Ordering

# GrowingSet
self: A ChangingSet
A ChangingObject with
operations = SequenceOf(An AddElementToSet)

# Interval↑11: HasFunctional(sequence, IntegerInterval, bottom, top)
bottom: An Integer
top: An Integer; Not(LessThan(My bottom))
sequence: A Sequence with
length = Sum(1, Difference(My top, My bottom))
pairs = SetOf(Satisfies
(Lambda(’Pair,
\A SequencePositionPair with
element = Sum(Difference(My bottom,1),
The position from a
SequencePositionPair
thatIs That(Pair)))))

# LambdaForm↑11: HasFunctional(self, Lambda, variable, form)
variable: Or(A LispAtom, SequenceOf(A LispAtom))
form: A DescriptionForm

# MapRangeDescription↑11: HasFunctional(range, MapSet, domain, form)
HasFunctional(rangeUnion, MapJoin, domain, form)
range: A Set
domain: A Set
rangeUnion: The union from a SetUnion with components = My range
mapping: A MathematicalMapping with
range = My range
domain = My domain
pairs =
SetOf(The pair from a LambdafiedPairDescription with
form = My form
form: A LambdaForm

# MathematicalMappingPair
self: <My domainElement, My rangeElment>
mapping: A MathematicalMapping
rangeElement: MemberOf(The range from My mapping)
domainElement: MemberOf(The domain from My mapping)

# MultipleLambdaConversion
lambdaForm: A LambdaForm with variable = SequenceOf(A LispAtom)
value: SequenceOf(A Thing)
convertedForm: A DescriptionForm

# OneOneMap↑11:FurtherSpecified(MathematicalMapping)
range: A Set with cardinality = The cardinality from My domain

# OrderedSetContainment↑1
1: HasFunctional(superset, SuperOrderOf, subset)
HasFunctional(subset, SubOrderOf, superset)
Comment ("The way this is defined, it is possible for the sub ordering
to leave out ordering pairs which hold between in the
superordering between elments which are in the subordering.
Is this the most useful definiition? should there be two?")
superset: An Ordering
subset: An Ordering with
elements = SubsetOf(The elements from My superset)
relation = The relation from My superset
pairs = SubsetOf(The pairs from My superset)

# Ordering↑11: HasFunctional(MemberOf minima, BottomElementOf, self)
HasFunctional(MemberOf maxima, TopElementOf, self)
elements: A Set
relation: An OrderingRelation
pairs: SetOf(An OrderPair with
ordering = My self
top = MemberOf(My elements)
bottom = MemberOf(My elements))
minima: ThoseIn(My elements,
Not(The top from an OrderPair thatIs
MemberOf(My pairs)))
maxima: ThoseIn(My elements,
Not(The bottom from an OrderPair thatIs
MemberOf(My pairs)))

# OrderingDescription↑1
1: HasFunctional(ordering, OrderingOf, quoted description)
ordering: An Ordering with
elements = SetOf(DescribedBy(My description))
description: A DescriptionForm

# OrderingRelation↑11: Comment("nothing about this has been defined yet")

# Partition↑11: FurtherSpecified(SetUnion)
HasFunctional(components, PartitionOf, union)
components: EveryChoice
(Lambda(<’x,’y>,
\Whose(’x, Not(HasMember (MemberOf(That(y))))))

# Queue
self: A ChangingSequence
A ChangingObject with
description = \A Sequence
operations =
SequenceOf(Or(An AddElementToBackOfSequence,
A RemoveElementFromFrontOfSequence))

# SequenceBackElement↑11: HasFunctional(long, AddBack, item, short)
HasFunctional(short, AllButLast, long)
short: A Sequence
item: A Thing
long: A Sequence
Concatenation(My short, <My Item>)

# SequenceConcatenation↑1
1: HasFunctional(fullSequence, Concatenation, sequence components)
HasFunctional(start, InitialSequenceOf, fullSequence)
HasFunctional(finish, FinalSequenceOf, fullSequence)
components: SequenceOf(A Sequence)
start: Nth(1, My components)
A Sequence with
pairs =MapSet(ThoseIn(The pairs from My fullSequence,
\A SequencePositionPair with
position = Not(GreaterThan
(The length from
A Sequence thatIs
My start))),
Lambda(’Pair,
\A SequencePositionPair with
element =
The element from
a SequencePositionPair
thatIs That(Pair)
position =
The position from
a SequencePositionPair
thatIs That(Pair)
finish: Using The length from My components
1 -> <>
2 -> Nth(2, My components)
GreaterThan(2)
-> The fullSequence from a SequenceConcatenation with
components = AllButFirst(My components)
A Sequence with
pairs =
MapSet(ThoseIn(The pairs from My fullSequence,
\A SequencePositionPair with
position = GreaterThan
(The length from
My start))
Lambda(’Pair
\A SequencePositionPair with
element = The element from
a SequencePositionPair
thatIs That(Pair)
position =
Difference
(The position from
a SequencePositionPair
thatIs That(Pair),
The length from My start))
fullSequence: A Sequence with length = Sum(The length from My start,
The length from My finish)

# SequenceContainment↑1
1: HasFunctional(subSequence, SubSequence, sequence)
sequence: A Sequence
Concatenation(My header, My subSequence, A Sequence)
firstPosition: An Integer
MemberOf(IntegerInterval(1, The length from My sequence))
Difference(1, The length from My header)
lastPosition: An Integer
MemberOf(IntegerInterval(1, The length from My sequence))
Sum(The length from My header, The length from My subSequence)
subSequence: A Sequence
header: A Sequence

# SequenceDescription↑1
1: HasFunctional(sequence, SequenceOf, quoted description)
sequence: A Sequence with
pairs = SetOf(A SequencePositionPair with
element = DescribedBy(My description))
description: A DescriptionForm

# SequenceEnumeration ↑11: Comment ("one of the descriptor types --
see that section for more information")
self: A DescriptorForm

# SequenceFrontElement↑11: HasFunctional(long, AddFront, item, short)
HasFunctional(short, AllButFirst, long)
short: A Sequence
item: A Thing
long: A Sequence
Concatenation(<My Item>, My short)

# SequenceMapping↑11: HasFunctional(range, MapSequence, domain, form)
HasFunctional (rangeJoin, SequenceJoin, domain, form)
domain: A Sequence
setMap: The mapping from a MapRangeDescription with
domain = The elements from My domain
form = My form
form: A DescriptorForm
rangeJoin: The fullSequence from a Concatenation with
components = My range
range: A Sequence with
pairs =
MapSet(The pairs from My domain,
Lambda(’Pair,
\A SequencePositionPair with
position =
The position from a SequencePositionPair
thatIs That(Pair)
element =
The rangeElement from
a Mathematical MappingPair with
domainElement =
The element from
a SequencePositionPair
thatIs That(Pair)
thatIs MemberOf(My setMap)))

# Set
cardinality: A CardinalNumber

# SetContainment↑11: HasFunctional(superset, SupersetOf, subset)
HasFunctional(subset, SubsetOf, superset)
HasFunctional(difference, SetDifference, superset, subset)
superset: A Set
subset: A Set; SetOf(MemberOf(My superset))
difference: SetOfAll(MemberOf(My superset)
Not(MemberOf(My subset)))

# SetElementDescription↑11: HasFunctional(set, SetOf, quoted description)
set: A Set
description: A DescriptionForm
Which↑2 Describes(MemberOf↑3(My set))
2: ForAll(Noteref 3)

# SetElementSufficientDescription↑11: HasFunctional(set, SetOfAll, quoted description)
set: A Set; SetOf(My description)
description: A DescriptionForm
Not(Which Describes (Not(MemberOf(My set)))

# SetEnumeration
self: A DescriptorForm

# SetIntersection↑11: HasFunctional(intersection, IntersectionOf, set components)
Comment("All of the union and intersection functionals take an
arbitrary length sequence of arguments")
components: SetOf(A Set)
intersection: SetOfAll(MemberOf↑2(MemberOf↑3(My components)))
2: ForAll(Noteref 3)

# SetMembership↑11: HasFunctional(element, ElementOf, set)
HasFunctional(difference, AllBut, element, set)
element: A Thing
set: A Set
difference: SetOfAll (ElementOf(My set)
Not(My element))

# SetSelection↑11: HasFunctional(subset, ThoseIn, superset, description)
description: A DescriptionForm
superset: A Set
subset: A Set
SetOfAll (MemberOf(My superset)
DescribedBy(My description))

# SetUnion↑11: HasFunctional(union, UnionOf, set components)
components: SetOf(A Set)
union: SetOfAll(MemberOf(MemberOf(My components)))

# SingleLambdaConversion
lambdaForm: A LambdaForm with variable = A LispAtom
value: A Thing
convertedForm: A DescriptionForm

# TotalOrdering
self: An Ordering with
elements =
EveryChoice
(Lambda(<’x,’y>,
\Or(Whose(’x, Follows(That(y), My self)),
Whose(’y, follows(That(x), My self)))))
sequence: A Sequence with elements = The elements from My self

# TransitiveClosure
ordering: An Ordering
given: SetOf(An OrderPair with ordering = My ordering)
closure:↑11: Comment ("This needs an appropriate recursive definition, but I don’t want to
take the time now")

# # # # # # # # # # # # # # #