Class FUNCTION

• Defined in theory: Kif-relations
• Source code: frame-ontology.lisp

Slots on this class:

Documentation:

A function is a mapping from a domain to a range that associates a domain element with exactly one range element. The elements of the domain are tuples, as in relations. The range is a class -- a set of singleton tuples -- and element of the range is an instance of the class. Functions are also first-class objects in the same sense that relations are objects: namely, functions can be viewed as sets of tuples.

Instance-Of: Class

Subclass-Of: Relation

Has-Instance:

*, +, -, /, 1+, 1-, Abs, Acos, Acosh, Adjoin, Append, Apply, Ash, Asin, Asinh, Atan, Atanh, Boole, Butlast, Ceiling, Cis, Complement, Composition, Conjugate, Cons, Cos, Cosh, Decode-float, Denominator, Difference, Exp, Expt, Fceiling, Ffloor, First, Float, Float-digits, Float-precision, Float-radix, Float-sign, Floor, Fround, Ftruncate, Gcd, Generalized-intersection, Generalized-union, Imagpart, Integer-decode-float, Integer-length, Intersection, Inverse, Isqrt, Last, Lcm, Length, Listof, Log, Logand, Logandc1, Logandc2, Logcount, Logeqv, Logior, Lognand, Lognor, Lognot, Logorc1, Logorc2, Logxor, Map, Max, Min, Mod, Nth, Nthrest, Numerator, Phase, Rationalize, Realpart, Rem, Remove, Rest, Revappend, Reverse, Round, Scale-float, Setof, Signum, Sin, Sinh, Sqrt, Subst, Tan, Tanh, Truncate, Union, Universe, Value

Superclass-Of:

Binary-function, Many-one, One-one, Unary-function

Equivalence Axioms:

(<=> (Function ?Relation)
     (And (Relation ?Relation)
          (Forall (?Tuple1 ?Tuple2)
                  (=> (Member ?Tuple1 ?Relation)
                      (Member ?Tuple2 ?Relation)
                      (= (Butlast ?Tuple1) (Butlast ?Tuple2))
                      (= (Last ?Tuple1) (Last ?Tuple2))))))

Axioms:

(Forall (?Tuple1 ?Tuple2)
        (=> (Member ?Tuple1 ?Relation)
            (Member ?Tuple2 ?Relation)
            (= (Butlast ?Tuple1) (Butlast ?Tuple2))
            (= (Last ?Tuple1) (Last ?Tuple2))))

(Relation ?Relation)

Other Related Axioms:

(<- (Value ?F @Args)
    (If (And (Function ?F)
             (Member ?List ?F)
             (= (Butlast ?List) (Listof @Args)))
        (Last ?List)))

(<- (Apply ?F ?List)
    (If (And (Function ?F) (= ?List (Listof @Args)))
        (Value ?F @Args)))

(Inherited-Facet-Value Slot-Value-Type One-One Inverse Function)

(<=> (One-One ?R)
     (And (Binary-Relation ?R)
          (Function ?R)
          (Value-Type ?R Inverse Function)
          (Value-Cardinality ?R Inverse 1)))

(<=> (Many-One ?R) (And (Binary-Relation ?R) (Function ?R)))

(Inherited-Facet-Value Slot-Value-Type One-Many Inverse Function)

(<=> (One-Many ?R)
     (And (Binary-Relation ?R)
          (Value-Type ?R Inverse Function)
          (Value-Cardinality ?R Inverse 1)))

(Instance-Of (Function (Inverse ?R)) Not)

(Not (Function (Inverse ?R)))

(Instance-Of (Function ?R) Not)

(Not (Function ?R))

(<=> (Many-Many ?R)
     (And (Binary-Relation ?R)
          (Not (Function ?R))
          (Not (Function (Inverse ?R)))))

(<=> (Unary-Function ?F) (And (Function ?F) (Binary-Relation ?F)))

(<=> (Binary-Function ?F)
     (And (Function ?F)
          (Not (Empty ?F))
          (Forall (?List) (=> (Member ?List ?F) (Triple ?List)))))

(<=> (Function ?Relation)
     (And (Relation ?Relation)
          (Forall (?Tuple1 ?Tuple2)
                  (=> (Member ?Tuple1 ?Relation)
                      (Member ?Tuple2 ?Relation)
                      (= (Butlast ?Tuple1) (Butlast ?Tuple2))
                      (= (Last ?Tuple1) (Last ?Tuple2))))))