Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

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

 實體

抽象的

關係

序列

## 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))```