xu4 lie4 (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)

shi2 ti3

chou1 xiang4 de5

guan1 xi4

xu4 lie4

Instance(s)

kong1 lie4

Subclass(es)

wei2 yi1 xu4 lie4

Coordinate term(s)

er4 yuan2 guan1 xi4 pian1 zhi2 guan1 xi4 shu4 ci2 huo4 ran2 lv4 guan1 xi4 si4 yuan2 guan1 xi4 wu3 yuan2 guan1 xi4 yu3 liang4 guan1 xi4 dan1 zhi2 guan1 xi4 kong1 jian1 guan1 xi4 shi2 jian1 guan1 xi4 san1 yuan2 guan1 xi4 quan2 zhi2 guan1 xi4 bian4 yi4 yuan2 shu4 guan1 xi4

Constrains relations

lie4 jie2 han2 shu4 xu4 lie4 han2 shu4 lie4 zhang3 han2 shu4 lie4 xu4 han2 shu4 cun2 zai4 suo3 you3 chuan4 lie4 zhong1 ci4 xu4 lie4

Related WordNet synsets

See more related synsets on a separate page.

Axioms (3)

guan1 xi4 wan2 quan2 fen1 ge1 cheng2 shu4 ci2,han2 shu4,xu4 lie4.

(partition Relation Predicate Function List)

if list shi4 xu4 lie4 de5 shi2 li4,
then there exists number1 so_that_not there exists item1 so_that_not "list de5 di4 er4 yuan2 su4" deng3 yu1 item1 and for all number2 holds: if number2 shi4 zheng4 zheng3 shu4 de5 shi2 li4 and number2 xiao3 yu1 number1, then there exists item2 so_that_not "list de5 di4 er4 yuan2 su4" deng3 yu1 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 shi4 xu4 lie4 de5 shi2 li4 and list2 shi4 xu4 lie4 de5 shi2 li4 and for all number holds: "list1 de5 di4 er4 yuan2 su4" deng3 yu1 "list2 de5 di4 er4 yuan2 su4", then list1 deng3 yu1 list2.

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