;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*- 
;;; 
;;;---------------------------------------------------------------------- 
;;; Knowledge Systems Laboratory, Stanford Univesity 
;;; Author: Adam Farquhar (Adam_Farquhar@ksl.stanford.edu) 
;;; Copyright (c) 1993 by Adam Farquhar. 
;;; 
;;; Some portions of this file come from the Engineering Math 
;;; Ontologies, which contain the following copyright: 
;;; 
;;; Physical Quantities Ontology, 
;;; Scalar Quantities, 
;;; Unary Scalar Functions, 
;;; (c) 1993 Greg Olsen and Thomas Gruber 
;;; 
;;;---------------------------------------------------------------------- 
;;; File Description: 
;;;    This file contains the ONTOLINGUA background definitions 
;;;    required for CML.  This file, together with the result of 
;;;    translating a closed domain theory should comprise a complete 
;;;    OL theory. 
;;; 
;;; History/Bugs/Notes: 
;;;   [axf 09/29/93] Created. 
;;; 
;;; - I dropped quantity-values.  They used to be 'things with 
;;; dimensions' that could be the value of a quantity.  Since I've 
;;; added ordinal and nominal quantities, which can have any objconst 
;;; as values, the class is no longer very meaningful.  Something that 
;;; means 'values-with-dimension' might be useful as a domain 
;;; restriction for relations on quantities such as <, +, sin, etc, 
;;; which have domains from the reals. 
;;; 
;;;---------------------------------------------------------------------- 
;;; 
;;; 

(in-package "ONTOLINGUA-USER") 

(define-theory CML (unary-scalar-functions standard-units) 

  "The CML ontology is the theory underlying the CML language.  It 
defines the basic concepts, such as model-fragment and 
time-dependent-relation, that are assumed in the language.  It gives 
axiomatic semantics for the notion of time and change inherent in CML. 
The CML ontology is built upon the Engineering Math ontologies, 
extending the unary-scalar-functions and standard-units theories.") 

(in-theory :CML) 

(define-class MODEL-FRAGMENT (?x) 

  "A MODEL-FRAGMENT instance describes an aggregate (perhaps empty) of 
participating objects under certain conditions." 

  :def (individual ?x) 
  ) 

(define-class ENTITY (?X) 

  "An ENTITY is an object with structurally stable properties.  It 
differs from a MODEL-FRAGMENT in the set of properties that make sense 
for it.  E.g.  an 'automobile' is naturally represented as an entity, 
which might have attributes such as color: red, manufacturer: ford.  " 

  :def (individual ?x)) 


(define-relation ACTIVE (?time ?model-fragment-class ?mf-instance) 
  "A model-fragment is associated with a set of time-dependent 
conditions and consequences; when those conditions hold, the 
consequences hold.  While conditions and consequences are time-dependent, 
the participants, attributes, and quantities associated with a model-fragment 
are part of its definition and the associations do not change over time. 
Similarly, model-fragment classes are organized in a class hierarchy, 
and a model-fragment instance can be an instance of more than one class. 
  The ACTIVE predicate associates a set of conditions with a model-fragment 
class.  A model fragment instance is active with respect to the 
conditions associated with a model-fragment class and a particular time. 
Thus, (active ?t ?mf-class ?mf-instance) holds when the conditions of 
the class ?mf-class, instantiated for instance ?mf-instance, 
are true at the time ?t. 
  The translation of CML forms into KIF produces axioms that determine 
when ACTIVE holds for particular model fragments." 
  :def (and (time-quantity ?time) 
	    (subclass-of ?model-fragment-class model-fragment) 
	    (model-fragment ?mf-instance))) 
   

(define-class INFINITE (?x) 

  "The class of infinite quantities which includes 
infinite quantities for every physical dimension." 

  :def (constant-quantity ?x)) 


(define-class SCENARIO (?s) 
    "A scenario is a description of a modeled system, a set of 
initial conditions for exogenous constants, and an interval of time 
over which the system is to be analyzed or simulated." 
  :def (and (individual ?s) 
	    (defined (initial-time ?s)) 
	    (time-quantity (initial-time ?s)) 
	    (defined (final-time ?s)) 
	    (time-quantity (final-time ?s)) 
	    (defined (scenario.participants ?s)))) 


(define-function INITIAL-TIME (?s) :-> ?t 
  "The initial time of a scenario is a time-quantity." 
  :def (and (scenario ?s) 
	    (time-quantity ?t))) 


(define-function FINAL-TIME (?s) :-> ?t 
  "The final time of a scenario is a time-quantity." 
  :def (and (scenario ?s) 
	    (time-quantity ?t))) 


(define-function SCENARIO.PARTICIPANTS (?s) :-> ?participants 
  "The scenario.participants of a scenario is a set of entities 
for which the scenario is defined." 
  :def (and (scenario ?s) 
	    (set ?participants) 
	    (=> (member ?p ?participants) 
		(entity ?p)))) 


(define-class PARTICIPANT-FUNCTION (?f) 
  "A participant function is a unary function from model fragments 
to entities." 
  :iff-def (and (unary-function ?f) 
		(domain ?f model-fragment) 
		(range ?f entity))) 


(define-class ATTRIBUTE-FUNCTION (?f) 
  "An attribute-function is a unary function defined over 
model fragments or entities." 
  :iff-def (and (unary-function ?f) 
		(domain ?f (kappa (?x) 
			      (or (model-fragment ?x) 
				  (entity ?x)))))) 

(define-function == (?q1 ?q2) 
  "== is equality between quantities, factoring out differences 
between constants and time-dependent quantities. 
A time-dependent quantity that always returns the same value 
is == to its value, but not = to its value." 
  :iff-def (and (physical-quantity ?q1) 
		(physical-quantity ?q2) 
		(forall ?t 
		  (= (value-at ?q1 ?t) (value-at ?q2 ?t))))) 

(define-class PIECEWISE-CONTINUOUS-QUANTITY (?x) 
  "If ?x is defined over some dense interval of ?t, then 
there are a finite number of points at which ?t is not 
continuous." 

  :def (function-quantity ?x) 

  :issues 
  (("A piecewise continuous quantity need not have a well defined value at 
a time point.  One needs to know the direction as well (from left or 
right).  Is is that the value not well defined, or is the means of 
finding the value not well defined?") 
   ("Note that the derivative of a standard-quantity may be a 
piecewise-continuous-quantity."))) 


(define-class EVERYWHERE-CONTINUOUS-QUANTITY (?x) 
  :def (and (piecewise-continuous-quantity ?x) 
	     ;; need to put in calculus for this 
	    ) 
  :issues 
  (("Should restrict the definition to apply to the dense intervals 
over which ?x is defined."))) 

(define-class STANDARD-QUANTITY (?x) 
  "A STANDARD-QUANTITY is everywhere continuous, has a piecewise 
continuous derivative, and a dimension. Quantities in QPT and QPC are 
standard-quantities.  In QSIM, the derivatives are continuous as well 
within a behavior." 
  :iff-def (and (everywhere-continuous-quantity ?x) 
                (piecewise-continuous-quantity (d/dt ?x)))) 


(define-class TIME-DEPENDENT-RELATION (?rel) 
    "Time dependent relations are relations whose first argument is a 
time quantity.  This is a second order relation." 
  :def (and (relation ?rel) 
	     ;; relation is of fixed arity 
	    (n-ary-relation ?rel) 
	     ;; the first argument is a time 
	    (nth-domain ?rel 1 time-quantity) 
	    )) 


(define-class TIME-DEPENDENT-FUNCTION (?f) 
  "Time dependent functions are functions whose first argument is a 
time quantity.  This is a second order relation." 
  :def (and (time-dependent-relation ?f) 
	    (function ?f))) 


(define-function VALUE-AT (?q ?time) :-> ?val 

  "The function value-at returns the value of a quantity at some point 
in time.  If the quantity is a function-quantity, then its value-at is 
its function value applied to the 'time' argument.  If the quantity is 
constant-quantity, then its value-at is the quantity itself for all 
'times'." 

  :def (and (quantity ?q) 
	    (time-quantity ?time)) 
  :lambda-body (if (function-quantity ?q) 
                   (value ?q ?time) 
		 ?q)) 

;;;---------------------------------------------------------------------- 
;;; We need polymorphic definitions for all of the operations allowed 
;;; on quantities. 
;;;---------------------------------------------------------------------- 

(define-relation M+ (?x ?y) 

  "The M+ relationship holds between two quantities x y exactly when 
y = f(x) and f is a monotonic increasing function." 

  :def (and (time-dependent-quantity ?x) 
            (time-dependent-quantity ?y))) 


(define-relation M- (?x ?y) 

  "The M- relationship holds between two quantities x y exactly when 
y = f(x) and f is a monotonic decreasing function." 

  :def (and (time-dependent-quantity ?x) 
            (time-dependent-quantity ?y))) 


(define-relation C+ (?x ?y) 

  "The C+ relation between two quantities x and y means 
that x = f(...,y,...) and the partial of f w.r.t. y is 1.  If all of 
the arguments to f are C+, this is equivalent to saying that x is 
their sum." 

  :def (and (time-dependent-quantity ?x) 
            (time-dependent-quantity ?y))) 

(define-relation C- (?x ?y) 

    "The C+ relation between two quantities x and y means 
that x = f(...,y,...) and the partial of f w.r.t. y is -1.  If all of 
the arguments to f are C+, this is equivalent to saying that -x is 
their sum." 

  :def (and (time-dependent-quantity ?x) 
            (time-dependent-quantity ?y))) 

(define-relation Qprop+ (?x ?y) 

  "The qualitative proportionality, Qprop+, also known as an indirect 
influence in the qualitative process theory literature, states that 
all things being equal ?x is proportional to ?y.  If there are no 
other influences on ?x, then (Qprop+ ?x ?y) is equivalent 
to (M+ ?y ?x).  Otherwise, it means that x = f(...,y,...) and the 
partial of f w.r.t. y is greater than zero." 

  :def (and (time-dependent-quantity ?x) 
            (time-dependent-quantity ?y))) 

(define-relation Qprop- (?x ?y) 

    "The qualitative proportionality, Qprop-, also known as an indirect 
influence in the qualitative process theory literature, states that 
all things being equal ?x is proportional to ?y.  If there are no 
other influences on ?x, then (Qprop- ?x ?y) is equivalent 
to (M- ?y ?x).  Otherwise, it means that x = f(...,y,...) and the 
partial of f w.r.t. y is less than zero." 

  :def (and (time-dependent-quantity ?x) 
            (time-dependent-quantity ?y))) 


(define-class QUANTITY-FUNCTION (?qf) 

  "A quantity function maps some objects to a quantity." 

  :def (and (function ?qf) 
	    (range ?qf time-dependent-quantity)) 
  :issues 
  (("Quantity functions defined within different model fragments may map 
to quantities with different dimensions and so on, so there is little 
that we can say about quantity functions beyond stating that the 
elements of their range is a quantity."))) 


(define-relation CONTINUOUS-AT (?f ?p) 
  "A function ?f is continuous at the point ?p." 
  :iff-def 
  (forall (?x ?epsilon) 
	  (=> (< (norm (value ?f ?p) (value ?f ?x)) ?epsilon) 
	      (exists (?delta) 
		      (< (norm (- ?x ?p) ?delta))))) 
  :issues ("THIS DEFINITION NEEDS WORK.")) 

(define-relation CONTINUOUS-OVER (?f ?beg ?end) 
  "A function ?f is continous over the interval ?beg ?end if it is 
defined and continuous-at every point between ?beg and ?end 
exclusive." 
  :iff-def (and (unary-scalar-function-quantity ?f) 
		(member ?beg (exact-domain ?f)) 
		(member ?end (exact-domain ?f)) 
		(forall (?x) 
		  (=> (and (< ?beg ?x) 
			   (< ?x ?end)) 
		      (and (defined (value ?f ?x)) 
			   (continuous-at ?f ?x)))))) 
	       



(define-relation piecewise-continuous-function (?f) 
  "A function is piecewise-continuous if it's domain can be 
partitioned into a sequence of intervals such that it is 
continuous-over each such interval, and there is a finite distance 
between each pair of break points." 
  ) 

(define-relation everywhere-continuous-function (?f) 
  "A function is everywhere-continuous if it is continuous over its 
entire domain." 
   ;; -- is this too strong?  Perhaps over every defined subsegment? 
  ) 


;;;---------------------------------------------------------------------- 
;;; Useful, but not necessary. 
;;;---------------------------------------------------------------------- 

(define-relation HAS-ATTRIBUTE-FUNCTION (?class ?attribute-function) 
  "A class has an attribute if the attribute value is given by a 
unary function, called an attribute-function, that is defined for 
that class." 

  :def (and (class ?class) 
            (attribute-function ?attribute-function) 
	    (attribute-function-of ?attribute-function ?class)) 

  ) 

(define-relation ATTRIBUTE-FUNCTION-OF (?function ?class) 
  :def (has-attribute-function ?class ?function)) 

(define-relation HAS-QUANTITY-FUNCTION (?class ?quantity-function) 
  "A class has an quantity if the quantity value is given by a 
unary function, called an quantity-function, that is defined for 
that class." 

  :def (and (class ?class) 
            (quantity-function ?quantity-function)) 

  ) 

(define-relation QUANTITY-FUNCTION-OF (?quantity-function ?class) 
  :def (has-quantity-function ?class ?quantity-function)) 

(define-relation PARTICIPANT-FUNCTION-OF (?function ?class) 
  :def (has-participant-function ?class ?function)) 

(define-relation HAS-PARTICIPANT-FUNCTION (?class ?function) 
  :def (and (class ?class) 
	    (participant-function ?function))) 


(define-function SLOT-DOCUMENTATION (?class ?unary-function) :-> ?doc 
  :iff-def (=> (instance-of ?instance ?class) 
               (documentation ?instance ?doc)) 

  :constraints (and (instance-of ?class class) 
                    (instance-of ?unary-function  unary-function)) 
  )