;;; -*- Mode:Lisp; Package:ONTOLINGUA-USER; Syntax:COMMON-LISP; Base:10 -*-
;;; Constraint Ontology
;;; (c) 1994 Thomas R. Gruber and Gregory R. Olsen
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; CONSTRAINT ONTOLOGY
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ONTOLINGUA-USER")
(define-theory PARAMETRIC-CONSTRAINTS (frame-ontology kif-meta)
"This theory provides the representational primitives for writing
parametric models with constraint expressions. It makes two basic
commitments: (1) Parameters are represented by normal object constants,
and the value of a parameter is its denotation. (2) Constraints are
reified objects, with quoted expressions that are KIF sentences;
constraint satisfaction is defined in terms of the truth value of the
sentences. This theory allows one to define embedded constraint
languages with the same syntax as KIF sentences but with restrictions
on the parameters, functions, and relations supported in the language.
This is critical for guaranteeing completeness or tractability of
constraint satisfaction.
The basic entities in this theory are PARAMETER-NAME (a symbol),
CONSTRAINT (an object), and CONSTRAINT-EXPRESSION (a sentence).
Parameter names are just KIF object constants. Constraints are objects
with an associated constraint-expression. A constraint-expression is a
special case of a KIF sentence. At the minimum, a
constraint-expression contains no quantifiers and has at most one free
variable; further restrictions on the form of a constraint expression
can be specified using RESTRICTED-CONSTRAINT-SENTENCE. The truth-value
semantics of constraints is defined in the predicates
SATISFIED-CONSTRAINT (for ground constraints) and
SATISFIES-CONSTRAINT (for constraints with a free variable).
Reifying parameters and constraints allows agents to talk about them as
objects in the universe of discourse, and to make inferences based on
meta-descriptions. For example, one would like to list the parameters and
constraints in a theory, distinguishing them from other axioms and
definitions. An agent could then analyze the constraints for completeness
without making closed world assumptions or second-order quantification.
Similarly, one could define sublanguages for which there are tractable
algorithms, but retain the common, declarative semantics of KIF.
This theory puts no limitations on what can be represented as parameters.
There is no special vocabulary for limit the \"possible values\" of a
parameter. Any restriction on the value of a parameter can be described with
a constraint. The meaning of parameters is also independent of any
object structure (i.e., parameters are not inherently properties of anything).
Specializations of this theory may define classes of constraints of
restricted form, and relate parameters to structured objects such as
components.
"
:issues ("(c) 1994 Thomas R. Gruber and Gregory R. Olsen"))
(in-theory 'PARAMETRIC-CONSTRAINTS)
(define-class PARAMETER-NAME (?p)
"In this theory, the relationship between a parameter and its value is the
same as between an object constant and its denotation. In a constraint
expression, one might see a symbol such as P1 occur as a term. According to
the normal semantics of KIF, an object constant is a symbol that denotes an
object in the universe of discourse. In engineering modeling, model
parameters (sometimes called variables) \"have a value\" -- which is
essentially the same idea as denotation. We wish to use the same semantics
as KIF for constraint languages used for engineering modeling. Therefore, we
use KIF object constants as parameters and take their detonation to be their
parameter value. However, since the notion of an object constant is more
general than engineering parameter, we need some way to distinguish the
latter. For this purpose we label some of the object constants (i.e., the
symbols) as parameter names. This lets us describe a set of parameters as a
set of names, rather than a set of values. Describing the set of values is
not sufficient because two parameters with the same values would be
indistinguishable.
For example, one might see the symbol P1 in a KIF sentence. The symbol \"P1\"
is an object constant. We might say that that P1 is equal to 10 with the KIF
sentence \"(= P1 10)\". We can say that the object constant \"P1\" is a
parameter-name in KIF as: (parameter-name 'P1). Then it follows that the
parameter.value of 'P1 is also its denotation: namely, 10. Now let's define a
second parameter P2 whose value is also 10. The two parameter names 'P1 and
'P2 are not the same parameter name, but they happen to have the same value.
Thus we can state the constraint (= P1 P2) using an ordinary KIF sentence,
while also allowing the distinction (not (= 'P1 'P2))."
:def (and (object-constant ?p)
(defined (parameter.value ?p))) ; it always has a value
:issues ((:example (parameter-name 'foo)
(not (parameter-name 10))
(not (parameter-name '(foo)))
(= foo (+ 10 20))
(= (parameter.value 'foo) 30))))
(define-function PARAMETER.VALUE (?parameter-name) :-> ?value
"Parameter.value is the function from parameter names to parameter
values. It is defined as a special case of KIF denotation: when given
an object constant that is a parameter-name, the parameter.value is
the denotation of the object constant. When given anything else, the
function is indefined (i.e., returns BOTTOM).
This theory does not put any restriction on the possible values of a
parameter. Such restrictions can be done with constraints on a per-model
basis."
:= (if (parameter-name ?parameter-name)
(denotation ?parameter-name)))
(define-class CONSTRAINT (?c)
"A constraint is a description that limits the permissible values for
parameters and other properties of objects in a design. In this
theory, constraints are objects with a slot called
constraint.expression, whose value is a KIF sentence of type
constraint-expression. This expression describes a constraint over
parameters mentioned in the constraint. The constraint expression may
also zero or one free variable. If the expression has not variables,
then the constaint is called a parametric-constraint -- it is only over
global parameters. If the expression contains a free variable, the
constraint is called an object-constraint -- the variable represents
the object being constrained.
The existence of a constraint does not imply that the
constraint.expression is a true sentence. The semantics of the
constraint expressions, including how \"binding\" to objects works, is
provided by the predicates SATISFIED-CONSTRAINT and
SATISFIES-CONSTRAINT. Satisfied-constraint is for parametric
constraints; in this case, the constraint is satisfied iff the sentence
is true. (Determining the truth of a constraint-expression may require
finding the values of parameters mentioned in the sentence, but these
parameters are not logical variables.) Object constraints are
satisfied with respect to some object. The predicate
SATISFIES-CONSTRAINT takes an object and a constraint-expression and
holds when the expression, with the object substituted for the free
variable, is a true sentence.
One may specify constraints with quoted expressions. For example,
for the constraint C1, we can say that its constraint expression is
a sentence relating two parameters, P1 and P2 as follows:
(= (constraint.expression C1) '(< P1 P2))
C1 is satisfied if the sentence '(< P1 P2) is true. If (= P1 10)
and (= P2 20), then (< P1 P2) and therefore C1 is satisfied."
:def (and
(defined (constraint.expression ?c)) ; must have an expression
(constraint-expression (constraint.expression ?c)))
:axiom-def (exhaustive-subclass-partition
CONSTRAINT
(setof parametric-constraint object-constraint))
:issues ((:example (constraint C1)
(= (constraint.expression C1)
'(< X Y)))
(:example (constraint C2)
(= (constraint.expression C2)
'(=> (> capacity 5000)
(= model-name "model 43b"))))
:see-also (SATISFIED-CONSTRAINT SATISFIES-CONSTRAINT)))
(define-function CONSTRAINT.EXPRESSION (?constraint) :-> ?expression
"Constraint.expression is a slot on constraint objects whose value is a KIF
sentence (the syntactic thing, a list expression). The form of the sentence
is limited by constraint-expression."
:def (and (constraint ?constraint)
(constraint-expression ?expression))
:issues ((:see-also constraint-expression)))
(define-function THE-CONSTRAINT (?expression) :-> ?constraint
"A constructor for constraint objects. Given a constraint
expression, it denotes the associated constraint object.
This means that constraints are uniquely defined by their
expressions."
:iff-def (and (constraint-expression ?expression)
(= (constraint.expression ?constraint) ?expression)))
(define-class CONSTRAINT-EXPRESSION (?sent)
"A contraint-expression is a KIF sentence with at most one free
variable denoting an object to which the constraint applies.
Other terms in the constraint-expression may be object constants
representing parameters, constant values like numbers and strings,
or other objects. The functions and relations that are allowed in
a constraint-expression are limited by restricted-constraint-sentence.
Restricted classes of constraints (subclasses of constraint-expression)
can be described by other applications of the restricted-constraint-sentence
predicate.
At the minimum, all constraint expressions have restricted quantification:
namely, no existential or universal quantification may be introduced
except for the optional single free variable. That is, the KIF operators
FORALL, EXISTS, SETOFALL, KAPPA, and LAMBDA are never allowed in constraint
expressions. Other restrictions on the constraint language may be specified
in specializations of the this class by giving different arguments to
the predicate restricted-constraint-sentence."
:def (restricted-constraint-sentence
?sent
logical-operator
relation-constant
function-constant
atomic-term)
:issues ((:see-also satisfied-constraint satisfies-constraint)))
(define-class PARAMETRIC-CONSTRAINT (?constraint)
"A parametric-constraint is a constraint whose constraint.expression
contains no variables. It's called parameteric because the
the things being constrained are parameters, rather than properties
of objects."
:iff-def (and (constraint ?constraint)
(ground-sentence (constraint.expression ?constraint)))
:issues ((:see-also SATISFIED-CONSTRAINT)))
(define-relation SATISFIED-CONSTRAINT (?constraint)
"A constraint is a SATISFIED-CONSTRAINT if its constraint.expression
is a true sentence. The sentence may contain no variables; that is,
the constraint must be a parametric-constraint."
:iff-def (and (parametric-constraint ?constraint)
(truth (constraint.expression ?constraint)))
:issues ("Whether a constraint is satisfied is not dependent
on any inference procedure or proof method. It does
not mean provable or derived. A parametric-constraint
is satisfied iff it is true."
"Satisfied-constraint is not the same as predicates
that are used to establish the truth of a sentence
relative to a theory or context."))
(define-class OBJECT-CONSTRAINT (?constraint)
"An object-constraint is a constraint on the properties of an object.
Such objects can represent arbitrary systems of objects and parameters;
this theory puts no restriction on the nature of the object (e.g., it
might be a component, or syntatic structure, or a list of parameters).
The purpose for distinguishing object constraints from parametric
constraints is to allow for a modular scope of a constraint.
Formally, an object-constraint is a constraint whose constraint.expression
is a sentence with one free variable. That variable is not universally
quantified; instead, it stands for the object being constrained.
The semantics of the constraint expressions is given by the predicate
SATISFIES-CONSTRAINT, which associates the variable with some specific
object."
:iff-def (and (constraint ?constraint)
(sentence-with-one-variable
(constraint.expression ?constraint))))
(define-relation SATISFIES-CONSTRAINT (?object ?constraint)
"An object-constraint is satisfied if its constraint.expression,
when applied to an object, is a true sentence.
The \"application\" of the expression is a syntactic construction
that transforms the expression into a KIF predicate. The constraint
is satisfied by an object iff the predicate holds for the object."
:iff-def
(and (object-constraint ?constraint)
(holds (denotation
(listof 'kappa
(listof (the-free-variable-in
(constraint.expression ?constraint)))
(constraint.expression ?constraint)))
?object))
:issues ("(KAPPA (?x) (p ?x)) denotes the relation that holds
for all ?x such that (P ?x) is true."
"(DENOTATION <expression>) refers to the the semantic value
of the expression. The semantic value of a KAPPA expression
is a unary relation."
"(HOLDS R a) means that the relation R holds on the object a.
A relation holds iff the associated predicate is true on
the arguments."
(:example (object-constraint C1)
(= (constraint.expression C1)
'(= (F ?x) (* (M ?x) (A ?x))))
(= (F body) 20)
(= (M body) 10)
(= (A body) 2)
(satisfies-constraint body C1))))
(define-relation RESTRICTED-CONSTRAINT-SENTENCE
(?sentence
?class-of-logical-operators
?class-of-relation-constants
?class-of-term-operators
?class-of-object-constants)
"restricted-constraint-sentence is a predicate used to specify
a class of sentences that are restricted by the set of operators
and terminals in the grammar.
The first argument is a KIF sentence, which must contain no
quantification (i.e., no use of FORALL, EXISTS, SETOFALL, LAMBDA,
or KAPPA).
The second argument is a class of logical operators (a class whose instances
are a subset of {AND, OR, NOT, =>, <=, <=>}).
The third argument is a class of relation constants, such as '< and '=.
The fourth argument is a class of function constants, such as + and FIRST.
The fifth argument is a class of object constants allowed, which is some
subset of OBJECT-CONSTANT. Instances of object-constant include
symbols, numbers, and strings, but not lists or variables. One can use this
argument to exclude some kinds of values by their syntatic form (e.g., strings)
or limit the set of symbols to some pre-enumerated set.
One can use this predicate to specify sublanguages within KIF, such as
constrain languages. One can denote classes of logical operators, relation
constants, and function constants using the ONE-OF function and giving it
quoted symbols as arguments. For example, the following specifies the
class of sentences without negation or implication, whose only functions
are the arithmetic operators, whose only relation is are equality, and whose
object constants are symbols and numbers:
(restricted-constraint-sentence ?sentence
(one-of 'and 'or 'not)
(one-of '=)
(one-of '+ '- '* '/)
(kappa (?x) (and (object-constant ?x) (not (string ?x)))))"
:iff-def (and (sentence ?sentence)
(not (quantsent ?sentence))
(subclass-of ?class-of-logical-operators
logical-operator)
(subclass-of ?class-of-relation-constants
relation-constant)
(subclass-of ?class-of-term-operators
function-constant)
(subclass-of ?class-of-object-constants
atomic-term)
(or
;; Relational Sentence
(exists (?r @tlist)
(and (= ?sentence (listof ?r @tlist))
(instance-of ?r ?class-of-relation-constants)
(=> (item ?t (listof @tlist))
(restricted-constraint-term
?t
?class-of-term-operators
?class-of-object-constants))))
;; like true or false
(truth-value-constant ?sentence)
;; Conjuction, Disjunction, Implication,
;; Reverse-Implication, or Equivalence
(exists (?op @sentences)
(and (= ?sentence (listof ?op @sentences))
(instance-of ?op ?class-of-logical-operators)
(=> (item ?s (listof @sentences))
(restricted-constraint-sentence
?s
?class-of-logical-operators
?class-of-relation-constants
?class-of-term-operators
?class-of-object-constants))))
)))
(define-relation RESTRICTED-CONSTRAINT-TERM (?term
?class-of-term-operators
?class-of-object-constants)
"This relation limits terms to atomic terms (variables or constants)
or to terms constructed via sanctioned term operators. No quantification
is allowed."
:iff-def (and
(term ?term)
(subclass-of ?class-of-term-operators
function-constant)
(subclass-of ?class-of-object-constants
atomic-term)
(or
;; a variable of constant reference
(instance-of ?term ?class-of-object-constants)
;; a valid operator over other terms: (+ v1 v2)
(exists (?oper @args)
(and (= ?term (listof ?oper @args))
(instance-of ?oper
?class-of-term-operators)
(=> (item ?arg (listof @args))
(restricted-constraint-term
?arg
?class-of-term-operators
?class-of-object-constants)))))))
(define-class ATOMIC-TERM (?x)
"An atomic-term is a KIF term that represents either a parameter
or a value. It cannot be a list expression; it must be a constant
or variable."
:iff-def (and (term ?x)
(not (list ?x))))
(define-class RELATION-CONSTANT (?r)
"A relation constant is a symbol that denotes a KIF relation."
:iff-def (relconst ?r))
(define-class OBJECT-CONSTANT (?C)
"An object constant is a symbol, a number specifier, or a string
that denotes some object in the universe of discourse."
:iff-def (objconst ?c))
(define-class FUNCTION-CONSTANT (?f)
"A function constant is a symbol that denotes a KIF function."
:iff-def (funconst ?f))
(define-class LOGICAL-OPERATOR (?op)
:iff-def (member ?op (setof 'not 'and 'or '=> '<= '<=>)))
(define-class TRUTH-VALUE-CONSTANT (?x)
"A truth-value constant is a symbol that denotes a logical
value of true or false. It is not a predicate!"
:iff-def (member ?x (setof 'true 'false)))
;; generic KIF expression machinery
(define-class GROUND-SENTENCE (?expression)
"A ground sentence contains no variables."
:iff-def (and (sentence ?expression)
(empty (variables-in-sentence ?expression))))
(define-function VARIABLES-IN-SENTENCE (?s) :-> ?vset
"This function takes an unquantified KIF sentence (the syntactic thing, an
expression) and returns the set of variables occuring freely in the sentence.
This is only defined for unquantified sentences, and only handles
individual variables (not sequence variables)."
:= (cond
;; If it starts with and, or, not, =>, <=>, /=,
;; then union the results of recursing on the enclosed sentences.
((logsent ?s)
(apply union
(map VARIABLES-IN-SENTENCE (rest ?s))))
;; If it is a relational sentence, such as (P a ?x),
;; then union the free variables found in each term expression.
((relsent ?s)
(apply union
(variables-in-term (rest ?s))))
;; if it is a logical constants, like TRUE,
;; then return the empty set
((logconst ?s)
(setof))
;; if it is a quantified sentence, like (forall ?x (p ?x)),
;; then the function is undefined. This will make the function
;; undefied if a quantified sentence occurs anywhere in the sentence.
((quantsent ?s)
bottom)))
(define-function VARIABLES-IN-TERM (?exp) :-> ?vset
"This function returns the set of free variables (individual variables)
that occur in an unquantified term expression. If there is a sequence
variable or quantified term expression, then this function is undefined."
:= (cond
;; if it is an individual constant, like ?X,
;; then return the singleton set containing it.
((indvar ?exp)
(setof ?exp))
;; (<function> [<term>]+)
((funterm ?exp)
(apply union
(map variables-in-term (rest ?exp))))
;; (IF <sent> <term> [<term>])
((and (logterm ?exp)
(= (first ?exp) 'IF))
(union
(variables-in-sentence (second-item ?exp))
(apply union
(map variables-in-term (rest (rest ?exp))))))
;; (COND [(<sent> <term>)]+)
((and (logterm ?exp)
(= (first ?exp) 'COND))
(apply union
(map variables-in-cond-clause (rest ?exp))))
;; SETOFALL, THE, KAPPA, LAMBDA -> undefined
((quanterm ?exp)
bottom)
;; other legitimate term, such as SETOF, LISTOF, QUOTE, or a constant
;; then return the empty set
((term ?exp)
(setof))))
(define-function VARIABLES-IN-COND-CLAUSE (?cond-clause) :-> ?vset
"COND clauses are of the form (sentence term)."
:= (if (and (list ?cond-clause)
(sentence (first ?cond-clause))
(term (second-item ?cond-clause)))
(union
(variables-in-sentence (first ?cond-clause))
(variables-in-term (second-item ?cond-clause)))))
(define-class SENTENCE-WITH-ONE-VARIABLE (?sentence)
:iff-def (and (sentence ?sentence)
(= 1 (cardinality (variables-in-sentence ?sentence)))))
(define-function THE-FREE-VARIABLE-IN (?sentence) :-> ?variable
"For sentences with exactly one free variable, this function
denotes that variable. It is otherwise undefined."
:= (if (sentence-with-one-variable ?sentence)
(the ?variable
(member ?variable (variables-in-sentence ?sentence))))
:constraints (indvar ?variable))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber