list (List)

Every List is a particular ordered n-tuple of items. Generally speaking, Lists are created by means of the ListFn Function, which takes any number of items as arguments and returns a List with the items in the same order. Anything, including other Lists, may be an item in a List. Note too that Lists are extensional - two lists that have the same items in the same order are identical. Note too that a List may contain no items. In that case, the List is the NullList.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

entity

abstract

relation

list

Instance(s)

null list

Subclass(es)

unique list

Coordinate term(s)

binary relation partial valued relation predicate probability relation quaternary relation quintary relation relation extended to quantities single valued relation spatial relation temporal relation ternary relation total valued relation variable arity relation

Constrains relations

list concatenate fn list fn list length fn list order fn exists forall in list sub list

Related WordNet synsets

See more related synsets on a separate page.

Axioms (3)

relation is exhaustively partitioned into predicate,function,list.

(partition Relation Predicate Function List)

if list is an instance of list,
then there exists number1 so that there exists item1 so that "number1th element of list" is not equal to item1 and for all number2 holds: if number2 is an instance of positive integer and number2 is less than number1, then there exists item2 so that "number2th element of list" is equal to item2

(=>
      (instance ?LIST List)
      (exists
            (?NUMBER1)
            (exists
                  (?ITEM1)
                  (and
                        (not
                              (equal
                                    (ListOrderFn ?LIST ?NUMBER1)
                                    ?ITEM1))
                        (forall
                              (?NUMBER2)
                              (=>
                                    (and
                                          (instance ?NUMBER2 PositiveInteger)
                                          (lessThan ?NUMBER2 ?NUMBER1))
                                    (exists
                                          (?ITEM2)
                                          (equal
                                                (ListOrderFn ?LIST ?NUMBER2)
                                                ?ITEM2))))))))

If list1 is an instance of list and list2 is an instance of list and for all number holds: "numberth element of list1" is equal to "numberth element of list2", then list1 is equal to list2.

(=>
      (and
            (instance ?LIST1 List)
            (instance ?LIST2 List)
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER)
                        (ListOrderFn ?LIST2 ?NUMBER))))
      (equal ?LIST1 ?LIST2))