zhi3 ding4 han2 shu4 (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)

zhong3 lei4

ke3 ji4 cheng2 guan1 xi4

han2 shu4

bian4 yi4 yuan2 shu4 guan1 xi4
is instance of

zhi3 ding4 han2 shu4

Coordinate term(s)

zui4 da4 gong1 yue1 shu4 han2 shu4 zui4 xiao3 gong1 bei4 shu4 han2 shu4 xu4 lie4 han2 shu4 mao2 dun4 shu3 xing4 wu2 jiao1 ji2 fen1 jie3 wu2 jiao1 ji2 guan1 xi4 qiong2 jin4 de5 shu3 xing4 qiong2 jin4 de5 fen1 jie3 cheng2 li4 fen1 ge1

Type restrictions

shi2 ti3 AssignmentFn(han2 shu4)

Axioms (10)

If function de5 fan4 wei2 shi4 class de5 shi2 li4 and "function()" deng3 yu1 value, then value shi4 class de5 shi2 li4.

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

If bei4 function gui1 hui2 de5 zhi2 shi4 classde5 ci4 zhong3 lei4 and "function()" deng3 yu1 value, then value shi4 class de5 ci4 zhong3 lei4.

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

If rel(,inst) (bu2) cheng2 li4s and rel shi4 han2 shu4 de5 shi2 li4, then "rel()" deng3 yu1 inst.

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

if fun shi4 yi1 dui4 yi1 han2 shu4 de5 shi2 li4,
then for all arg1,arg2 holds: if fun de5 lun4 yuan2 shi4 class de5 shi2 li4 and arg1 shi4 class de5 shi2 li4 and arg2 shi4 class de5 shi2 li4 and arg1 deng3 yu1 arg2, then "fun(arg1)" deng3 yu1 "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 shi4 guan1 lian2 han2 shu4 de5 shi2 li4,
then for all inst1,inst2,inst3 holds: if function de5 lun4 yuan2 shi4 class de5 shi2 li4 and inst1 shi4 class de5 shi2 li4 and inst2 shi4 class de5 shi2 li4 and inst3 shi4 class de5 shi2 li4, then "function(inst1,"function(inst2,inst3)")" deng3 yu1 "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 shi4 ke3 huan4 han2 shu4 de5 shi2 li4,
then for all inst1,inst2 holds: if function de5 lun4 yuan2 shi4 class de5 shi2 li4 and inst1 shi4 class de5 shi2 li4 and inst2 shi4 class de5 shi2 li4, then "function(inst1,inst2)" deng3 yu1 "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 feng1 bi4 yu1 class and function shi4 yi1 yuan2 han2 shu4 de5 shi2 li4,
then for all inst holds: if inst shi4 class de5 shi2 li4, then "function(inst)" shi4 class de5 shi2 li4

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

if function feng1 bi4 yu1 class and function shi4 er4 yuan2 han2 shu4 de5 shi2 li4,
then for all inst1,inst2 holds: if inst1 shi4 class de5 shi2 li4 and inst2 shi4 class de5 shi2 li4, then "function(inst1,inst2)" shi4 class de5 shi2 li4

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

if fen1 pei4(function1,function2) holds,
then for all inst1,inst2,inst3 holds: if function1 de5 lun4 yuan2 shi4 class1 de5 shi2 li4 and inst1 shi4 class1 de5 shi2 li4 and inst2 shi4 class1 de5 shi2 li4 and inst3 shi4 class1 de5 shi2 li4 and function2 de5 lun4 yuan2 shi4 class2 de5 shi2 li4 and inst1 shi4 class2 de5 shi2 li4 and inst2 shi4 class2 de5 shi2 li4 and inst3 shi4 class2 de5 shi2 li4, then "function1(inst1,"function2(inst2,inst3)")" deng3 yu1 "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 shi4 function de5 tong2 yi1 yuan2 su4,
then for all inst holds: if function de5 lun4 yuan2 shi4 class de5 shi2 li4 and inst shi4 class de5 shi2 li4, then "function(id,inst)" deng3 yu1 inst

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