(define-function <function-name> (<var>+)
[<docstring>]
[:-> <result-var>]
[<docstring>]
[:when <sent-with-arg-vars>]
[{:def | :iff-def} <sent-with-arg-vars>]
[:constraints <sent-with-arg-vars>]
[:axiom-def <sent-without-arg-vars>]
[:axiom-constraints <sent-without-arg-vars>]
[{:lambda-body | :=} <term-expression-with-arg-vars>]
[:theory <theory-name>]
[:implementation <target-system-name>]
[:issues <issue-tree>]
[:documentation <docstring>]
[:result-variable <var>])
Macro for defining OntoLingua functions. No arguments are evaluated. See also CREATE-FUNCTION, which is the functional form. Macro for defining OntoLingua functions and procedural attachments. No arguments are evaluated. See also CREATE-FUNCTION, which is the functional form.
<function-name> should be a symbol which names the function being defined. OntoLingua will convert this symbol into a format which is appropriate for the selected target representation system during translation (e.g., if one were translating into CycL, the symbol would be converted into a string which would obey the CycL conventions for case and word delimiters.)
<result-var> Just like an argument <var>, but it stands for the result of the function.
<docstring> when provided, should be a string which describes the function being defined. It will be stored as the Lisp documentation of type OL:ONTO-FUNCTION for the symbol which names the function, and used in pretty-printed ontology reports. If a docstring is provided, it must immediately follow the :-> argument (or immediately follow the argument list if no :-> argument is provided.)
<var> should be a KIF individual variable which serves as an argument to the function. Within the body of the DEFINE-FUNCTION form, there may be KIF sentences which refer to such a symbol as a variable in order to establish the constraints between the arguments to the function being defined and its value. Such constraints constitute the definition of an OntoLingua function. The <var> variables in the argument list may also be used as formal arguments in a procedural attachment.
The remaining keyword arguments may occur in any order, and are described below:
:AXIOM-CONSTRAINTS - The associated value should be a KIF sentence which is a standalone sentence not related to the variables in the argument list. It is the same as the :AXIOM-DEF sentence except it is not definitional -- relevant to the form being defined, but not part of its definition.
Logically, this sentence neither implies nor is implied by the relation holding for a given binding of the variable(s) <var> ; it is a standalone sentence. It should mention the relation being defined, however.
A list of sentences may be supplied instead of a single sentence; Ontolingua will automatically construct a conjunction of all the supplied :AXIOM-CONSTRAINTS sentences in this case.
:AXIOM-DEF - The associated value should be a KIF sentence to be asserted along with the definition of the function. Logically, this sentence stands alone, and has no relation to the variables in the argument list or the <RESULT-VARIABLE>. Terminologically, this sentence is considered definitional.
Second order sentences may be specified here (see Second Order Sentences)
For example:
(define-function identity (?anything) :-> ?same-thing
"returns its argument."
:lambda-body ?anything
:axiom-def (and (symmetric-function identity)
(transitive-function identity)))
The fact that the function identity is symmetric and transitive is considered to be part of the definition of identity.- The value should be a KIF sentence with no free variables. In particular, the sentence does not implicitly constrain the variables in the argument list (that is what :def and :iff-def are for). The :AXIOM-DEF sentence is considered to be definitional. That is, it is part of the definition as are :DEF and :IFF-DEF sentences. Non-definition axioms should be specified with the :AXIOM-CONSTRAINTS keyword.
A list of sentences may be supplied instead of a single sentence; Ontolingua will automatically construct a conjunction of all the supplied :AXIOM-DEF sentences in this case.
:CONSTRAINTS - The value of this keyword argument should be a list of KIF sentences which refer to the free variables in the the argument list and the <RESULT-VARIABLE> that are not meant as part of the definition.
:CONSTRAINTS sentences are logically equivalent to :DEF sentences. The purpose of the distinction between definitional and nondefinitional constraints is to support terminological reasoning apart from other types of deductive inference. The :CONSTRAINTS sentences are assertions used in nonterminological inference.
A list of sentences may be provided instead of a single sentence; OntoLingua automatically constructs a conjunction of all the supplied :CONSTRAINTS sentences in this case.
:DEF - The value of this keyword argument should be a KIF sentence which refers to the free variables in the argument list and the RESULT-VARIABLE. Logically, the :DEF sentence is "implied by" the function; i.e. the :DEF sentence holds for every variable binding such that the value of the function when applied to the variables in the argument list is the value of the RESULT-VARIABLE.
:DOCUMENTATION - when provided, should be a string which describes the function being defined. It will be stored as the Lisp documentation of type OL:ONTO-FUNCTION for the symbol which names the function, and used in pretty-printed ontology reports. If a docstring is provided, it must immediately follow the :-> argument (or immediately follow the argument list if no :-> argument is provided.)
:IFF-DEF - The value of this keyword argument should be a list of KIF sentences which refer to the free variables in the argument list and the RESULT-VARIABLE. Logically, the :IFF-DEF sentence both "implies" and "is implied by" the function; i.e. in addition to the property ascribed to the :DEF sentence above, for every variable binding such that the :IFF-DEF sentence holds, the value of the function applied to the variables in the argument list is the value of the RESULT-VARIABLE.It is not legal use both the :DEF and :IFF-DEF keywords in the same definition.
:IMPLEMENTATION - The value of this keyword argument should be a symbol (usually a keyword) which names the target representation system in which the definition should be defined. This is independent of the theory in which the defined is defined. If the :IMPLEMENTATION argument is not supplied, the current implementation is assumed (see IN-IMPLEMENTATION.)
:ISSUES - The value of this argument should be a Lisp "tree" of strings. The tree can be either a string, or a list of strings, or a list of (<label> <any-lisp-object>) pairs, where <label> is a string or symbol that names the type of the comment. For examples,
:issues ("This is a footnote about FOO."
(:example (= (foo ?x) (inverse (bar ?x))))
("Why not do it this way?
:THEORY - The value of this keyword argument should be a symbol which names the theory in which the definition should be defined. If the :THEORY argument is not supplied, the current theory is assumed (see IN-THEORY.)
:WHEN - this keyword provides a syntax for writing polymorphic function definitions. Polymorphism allows more than one definition of the same function. Each definition contributes a partial constraint (e.g., expresssion for determining the result of the function, or range constraint) depending on a predicate over the arguments to the function. For example, one could define extensions to the + function for sets, as follows:
(define-function + (?x ?y) :-> ?z
:when (and (set ?x) (set ?y))
:lambda-body (union ?x ?y))
or alternatively,
(define-function + (?x ?y) :-> ?z
:when (and (set ?x) (set ?y))
:iff-def (= ?z (union ?x ?y)))
The value of the :WHEN argument should be a KIF sentence which refers to the free variables in the argument list.
:=, and :LAMBDA-BODY - The value of this keyword argument should be a KIF term expression (a sentence denoting and object, not a truth value) which, when given bindings for the variables in ARGUMENT-LIST, can produce a value for the function. Logically, the fact that the result variable is equivalent to the :LAMBDA-BODY expression implies and is implied by the fact that the value of the function applied to the variables in ARGUMENT-LIST is the value of the RESULT-VARIABLE, for all variable bindings.
For example, the following form defines the 'feature value' of a feature in a simulation:
(define-function val (?feature ?step) :-> ?value
"function that returns the value of a DSL feature.
It dispatches on the type of the feature."
:def (and (feature ?feature)
(timepoint ?step)
(feature-value ?value))
:lambda-body (cond ((constant-feature ?feature)
(initial-value ?feature))
((connected-feature ?feature)
(val (source ?feature) ?step))
((functional-feature ?feature)
(valcompute ?feature ?step))
((markov-feature ?feature)
(if (= ?step 1)
(initial-value ?feature)
(valcompute ?feature (1- ?step))))))
:RESULT-VARIABLE, and :-> - The value of this keyword argument should be a symbol which will be used to represent the result of the function within the KIF sentences of the definition. It is not necessary to explicitly supply a result variable to talk about the result of the function. If this keyword argument is supplied, however, it must immediately follow the argument list.
Second Order Sentences
Within the :AXIOM-DEF there may be sentences that specify properties of the relation being defined, rather than properties of the instances related by the relation being defined. Such sentences use the names of relations as arguments to special "second order" relations. For example, consider the following definition:
(define-relation in-module (?port ?module)
"Function from a port to its associated module.
Each port has at most one associated module."
:def (and (port ?port)
(module ?module))
:axiom-def (SINGLE-VALUED in-module))
In the :AXIOM-DEF sentence, IN-MODULE is said to be a SINGLE-VALUED relation, which means:
(=> (and (in-module ?x ?y) (in-module ?x ?z)) (= ?y ?z))
The symbol IN-MODULE denotes the relation of that name. Since the argument to SINGLE-VALUED, IN-MODULE, is also a relation, SINGLE-VALUED is called a second-order relation.
Second order relations capture many conventions for defining and organizing terms in concise ways. For example, in the following definition, MODULE-PORTS is defined as the inverse of IN-MODULE. That is all that needs to be stated about this term; everything true of IN-MODULE is true of MODULE-PORTS with its arguments reversed:
(define-relation module-ports (?module ?port)
"The ports associated with a module."
:axiom-def (INVERSE module-ports in-module))
Terminologically, second-order sentences are always considered to be definitional. Only a restricted set of second-order relations are allowed; these are defined in the frame ontology.Alternate Slot Syntax
Ontolingua supports additional syntax for writing some definition sentences in a frame/slot style instead of the predicate calculus style of KIF. This additional syntax is supported via three additional definition keywords, whose associated values are lists of sentences in the following format, called a SLOT-VALUE-SPEC:
(slot-name slot-value1 slot-value2 ...)
SLOT-NAME is the name of a binary relation. The first argument to this binary-relation (the frame) is made implicit by the keyword with which the sentence is associated, and each SLOT-VALUE is a second argument to the relation.
During the translation process, Ontolingua will transform such a sentence into the equivalent KIF sentences
(slot-name frame slot-value-1)
(slot-name frame slot-value-2)
These resulting sentences will be added to the :AXIOM-DEF, :CONSTRAINTS, :AXIOM-CONSTRAINTS, or :DEFAULT-CONSTRAINTS sentences depending on the keyword with which the original slot-syntax sentences are associated.
The three keywords supported in this manner are as follows:
:CLASS-SLOTS - The associated value should be a list of SLOT-VALUE-SPECs whose frames are taken to be the relation being defined. Thus, the relations corresponding to the slot names are second-order relations (see "Second Order Sentences" above.) Sentences translated from :CLASS-SLOTS are added to the :AXIOM-DEF sentence.
:INSTANCE-SLOTS - This keyword is only valid in the definition of unary relations (or equivalently, classes.) The associated value should be a list of SLOT-VALUE-SPECs sentences whose frames are taken to be individuals for which the unary relation holds. Sentences translated from :INSTANCE-SLOTS are added to the :CONSTRAINTS sentence.
An extended slot syntax is supported for this keyword which allows values for "facets" of slots to be provided. Within the SLOT-VALUE-SPECS any of the slot-values may be a list of the form:
(facet facet-value1 facet-value2 ...)
Ontolingua will transform these into the equivalent KIF sentences:
(facet relation slot facet-value1) (facet relation slot facet-value2)
:DEFAULT-SLOT-VALUES - This keyword is only valid in the definition of unary relations (or equivalently, classes.) The associated value should be a list SLOT-VALUE-SPECs sentences whose frames are taken to be individuals for which the unary relation holds. Sentences translated form :DEFAULT-SLOT-VALUES are added to the :DEFAULT-CONSTRAINTS sentences, and will therefore hold for each instance of the class until and unless a contrary assertion is made about that instance.