序列 (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)

實體

抽象的

關係

序列

Instance(s)

空列

Subclass(es)

唯一序列

Coordinate term(s)

二元關係偏值關係述詞或然率關係四元關係五元關係與量關係單值關係空間關係時間關係三元關係全值關係變異元數關係

Constrains relations

列結函數序列函數列長函數列序函數存在所有串列中次序列

Related WordNet synsets

See more related synsets on a separate page.

Axioms (3)

關係完全分割成述詞,函數,序列.

(partition Relation Predicate Function List)

if list 是序列的實例,
then there exists number1 so that there exists item1 so that "list 的第二元素" 等於 item1 and for all number2 holds: if number2 是正整數的實例 and number2 小於 number1, then there exists item2 so that "list 的第二元素" 等於 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 是序列的實例 and list2 是序列的實例 and for all number holds: "list1 的第二元素" 等於 "list2 的第二元素", then list1 等於 list2.

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