Function Arity

Arity: 2
Definition-Sort-Index@Interface-Ontology: -100
Documentation:
Arity is the number of arguments that a relation can take. If a relation can take an arbitrary number of arguments, its arity is undefined. For example, a function such as `+' is of undefined arity; its last formal argument is specified with a sequence variable. The arity of a function is one more than the number of arguments it can take, in keeping with the unified treatment of functions and relations. The arity of the empty relation (i.e., with no tuples) is undefined.

Notes:

  • KIF 2.2 doesn't require one to declare the arity of a relation, nor does it require one to use a relation with a consistent number of arguments. However, relations defined with Ontolingua are always of fixed arity, which Ontolingua asserts as part of the translation. This is to facilitate sharing over implemented frame systems, most of which do not support variable-arity relations.
  • Asserting that the arity is undefined is not the same as saying that the arity is unconstrained. The arity can only exist if the relation is of fixed arity. Asserting (undefined (arity ?relation)) means that one knows that the relation has variable arity.
Domain: Relation
Instance-Of:
Binary-Relation, Binary-Relation, Function, Function, Function ...
Range: Integer

Equivalence Axioms for Arity:

(<=> (Arity ?Relation)
     (And (Relation ?Relation)
          (Not (Empty ?Relation))
          (Integer ?N)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (= (Length ?Tuple) ?N)))))

Frame References to Arity:

In class Show-All-Values-Slot@Interface-Ontology:

Arity: 1

In relation Subset:

Arity: 2

In function Inverse:

Arity: 2

In class Operator:

Arity: 1

In relation After=@Simple-Time:

Arity: 2

In relation Before@Simple-Time:

Arity: 2
...

Implication Axioms mentioning Arity:

(=> (= (Arity ?Relation) ?N)
    (Forall (?Tuple)
            (=> (Member ?Tuple ?Relation) (= (Length ?Tuple) ?N))))

(=> (= (Arity ?Relation) ?N) (Integer ?N))

(=> (= (Arity ?Relation) ?N) (Not (Empty ?Relation)))

(=> (= (Arity ?Relation) ?N) (Relation ?Relation))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (=< ?Column (Arity ?Relation)))

Equivalence Axioms mentioning Arity:

(<=> (Class ?Class) (And (Relation ?Class) (= (Arity ?Class) 1)))

(<=> (Projection ?Relation ?Column)
     (And (Defined (Arity ?Relation))
          (Positive-Integer ?Column)
          (=< ?Column (Arity ?Relation))
          (Class ?Projection-Relation)
          (Forall (?Projection-Instance)
                  (<=> (Instance-Of ?Instance ?Projection-Relation)
                       (Exists (?Tuple)
                               (And (Member ?Tuple ?Relation)
                                    (= (Nth ?Tuple ?Column)
                                       ?Instance)))))))

(<=> (Nth-Domain ?Relation ?N ?Type)
     (And (Defined (Arity ?Relation))
          (Positive-Integer ?N)
          (Class ?Type)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (And (>= (Length ?Tuple) ?N)
                           (Instance-Of (Nth ?Tuple ?N) ?Type))))))

Axioms mentioning Arity:

(<= (Arity ?X 1) (Class ?X))

(<= (Arity ?X 3) (Facet ?X))

(Undefined (Arity One-Of))

(Undefined (Arity Compose))

(Defined (Arity ?Relation))