指定函數 (AssignmentFn)

If F is a function with a value for the objects denoted by N1,..., NK, then the term (AssignmentFn F N1 ... NK) denotes the value of applying F to the objects denoted by N1,..., NK. Otherwise, the value is undefined.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

種類

可繼承關係

函數

變異元數關係

指定函數

Coordinate term(s)

最大公約數函數最小公倍數函數序列函數矛盾屬性無交集分解無交集關係窮盡的屬性窮盡的分解成立分割

Type restrictions

實體 AssignmentFn(函數)

Axioms (10)

If function 的範圍是 class 的實例 and "function()" 等於 value, then value 是 class 的實例.

(=>
      (and
            (range ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (instance ?VALUE ?CLASS))

If 被 function 歸回的值是 class的次種類 and "function()" 等於 value, then value 是 class 的次種類.

(=>
      (and
            (rangeSubclass ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (subclass ?VALUE ?CLASS))

If rel(,inst) (不) 成立s and rel 是函數的實例, then "rel()" 等於 inst.

(=>
      (and
            (holds ?REL @ROW ?INST)
            (instance ?REL Function))
      (equal
            (AssignmentFn ?REL @ROW)
            ?INST))

if fun 是一對一函數的實例,
then for all arg1,arg2 holds: if fun 的論元是 class 的實例 and arg1 是 class 的實例 and arg2 是 class 的實例 and arg1 等於 arg2, then "fun(arg1)" 等於 "fun(arg2)"

(=>
      (instance ?FUN OneToOneFunction)
      (forall
            (?ARG1 ?ARG2)
            (=>
                  (and
                        (domain ?FUN 1 ?CLASS)
                        (instance ?ARG1 ?CLASS)
                        (instance ?ARG2 ?CLASS)
                        (not
                              (equal ?ARG1 ?ARG2)))
                  (not
                        (equal
                              (AssignmentFn ?FUN ?ARG1)
                              (AssignmentFn ?FUN ?ARG2))))))

if function 是關連函數的實例,
then for all inst1,inst2,inst3 holds: if function 的論元是 class 的實例 and inst1 是 class 的實例 and inst2 是 class 的實例 and inst3 是 class 的實例, then "function(inst1,"function(inst2,inst3)")" 等於 "function("function(inst1,inst2)",inst3)"

(=>
      (instance ?FUNCTION AssociativeFunction)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS)
                        (instance ?INST3 ?CLASS))
                  (equal
                        (AssignmentFn
                              ?FUNCTION
                              ?INST1
                              (AssignmentFn ?FUNCTION ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION
                              (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                              ?INST3)))))

if function 是可換函數的實例,
then for all inst1,inst2 holds: if function 的論元是 class 的實例 and inst1 是 class 的實例 and inst2 是 class 的實例, then "function(inst1,inst2)" 等於 "function(inst2,inst1)"

(=>
      (instance ?FUNCTION CommutativeFunction)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))

if function 封閉於 class and function 是一元函數的實例,
then for all inst holds: if inst 是 class 的實例, then "function(inst)" 是 class 的實例

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION UnaryFunction))
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (instance
                        (AssignmentFn ?FUNCTION ?INST)
                        ?CLASS))))

if function 封閉於 class and function 是二元函數的實例,
then for all inst1,inst2 holds: if inst1 是 class 的實例 and inst2 是 class 的實例, then "function(inst1,inst2)" 是 class 的實例

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION BinaryFunction))
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (instance
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        ?CLASS))))

if 分配(function1,function2) holds,
then for all inst1,inst2,inst3 holds: if function1 的論元是 class1 的實例 and inst1 是 class1 的實例 and inst2 是 class1 的實例 and inst3 是 class1 的實例 and function2 的論元是 class2 的實例 and inst1 是 class2 的實例 and inst2 是 class2 的實例 and inst3 是 class2 的實例, then "function1(inst1,"function2(inst2,inst3)")" 等於 "function2("function1(inst1,inst2)","function1(inst1,inst3)")"

(=>
      (distributes ?FUNCTION1 ?FUNCTION2)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION1 1 ?CLASS1)
                        (instance ?INST1 ?CLASS1)
                        (instance ?INST2 ?CLASS1)
                        (instance ?INST3 ?CLASS1)
                        (domain ?FUNCTION2 1 ?CLASS2)
                        (instance ?INST1 ?CLASS2)
                        (instance ?INST2 ?CLASS2)
                        (instance ?INST3 ?CLASS2))
                  (equal
                        (AssignmentFn
                              ?FUNCTION1
                              ?INST1
                              (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION2
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))

if id 是 function 的同�@元素,
then for all inst holds: if function 的論元是 class 的實例 and inst 是 class 的實例, then "function(id,inst)" 等於 inst

(=>
      (identityElement ?FUNCTION ?ID)
      (forall
            (?INST)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?ID ?INST)
                        ?INST))))