O PT Manual Version 1.7.3 (Reflects Opt Version 1.6.11) * DRAFT ** Drew McDermott November 13, 2005 Change history: V. 1.7 2004-07-19 Document web mode and namespace mode Contents 1 Introduction and Overview 2 2 Technicalities 4 2.1 Syntactic Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 The Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 The Logical Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3 Built-in Types: Primitives, Fluents, Expressions 16 4 Domains 18 5 Actions 21 5.1 Syntax of Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 5.2 Effects and Values of Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.3 Effects Involving Fluents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6 Time and Processes 24 6.1 Process Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.2 Durative Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 7 Action Expansions 33 8 Facts and Axioms 38 9 Adding Facts and Action Expansions Modularly 40 10 Situations, Contexts, and Problems 41 11 Web Mode and Namespaces 44 1 12 Scope of Names 47 13 Built-in Symbols 48 13.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 13.2 Requirement Flags . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 13.3 Built-in Constants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1 Introduction and Overview O PT stands for Ontology with Polymorphic Types. It is an attempt to create a general-purpose notation for creating ontologies, defined as formalized conceptual frameworks for domains about which programs are to reason. Its syntax is based on PDDL [?], but it has a more elaborate type system, which allows users to make use of higher-order constructs such as explicit λ-expressions. O PT is intended to be (almost) upwardly compatible with PDDL 2.1, the dialect used in the 2002 International Planning Competition. Some of the prose in this document is lifted is lifted straight from previous PDDL documentation (which in turn may have been lifted from the UNPOP language manual). Where O PT differs from PDDL 2.1, I will point out how it differs. Opt borrows much of its notation for processes and durative actions from [?]. It’s my hope that PDDL will in fact evolve in the direction of O PT, but even if it doesn’t, O PT will continue to include PDDL as a subset for obvious reasons. [[One difference between lang and PDDL is that less of an effort has been made in the design of lang to separate “advice” from “physics.” Then again, the effort was a bit ill defined even for PDDL.]] In O PT, as in PDDL, a formalized ontology is called a domain. Domains can be related by inheritance relations, so very general ontologies can be used over and over. Not all domains involve the same level of expressivity. For example, some domains may be based on the assumption that any variable-free atomic formula not known to be true may be assumed to be false; this is called a “closed-world assumption.” In fact, this is the default in O PT, as in many AI applications, because closed worlds tend to be more tractable. However, there are domains where such an assumption is inappropriate, in which case verifying that a proposition is false requires a more substantial infer- ence than failing to prove it true. To control these differing kinds of domains, we borrow from the UCPOP language [?] the idea of requirements flags. Any domain that departs from the simplest subset of O PT must declare the requirements that it is based on (define (domain astronomy) (:requirements :open-world) ...) In this case we say that astronomy declares the requirement :open-world. Here is an example domain, a simple version of an ontology for an agent on the World-Wide Web: (define (domain www-agents) (:extends knowing regression-planning commerce) (:requirements :existential-preconditions :conditional-effects) (:types Message - Obj Message-id - String •) (:type-fun (Key t) (Feature-type (keytype t))) 2 (:type-fun (Key-pair t) (Tup • (Key t) t)) (:functions (price-quote ?m - Money) (query-in-stock ?pid - Product-id) (reply-in-stock ?b - Boolean) - Message) (:predicates (web-agent ?x - Agent) (reply-pending a - Agent id - Message-id msg - Message) (message-exchange ?interlocutor - Agent ?sent ?received - Message ?eff - Prop) (expected-reply a - Agent sent expect-back - Message)) (:facts (freevars (?agt - Agent ?msg-id - Message-id ?sent ?reply - Message) (<- (and (web-agent ?agt) (reply-pending ?agt ?msg-id ?sent) (expected-reply ?agt ?sent ?reply)) (normal-value (receive ?agt ?msg-id) ?reply)))) (:action (send ?agt - Agent ?sent - Message) - (?sid - Message-id) :precondition (web-agent ?agt) :effect (reply-pending ?agt ?sid ?sent)) (:action (receive ?agt - Agent ?sid - Message-id) - (?received - Message) :vars (?sent - Message ?eff - Prop) :precondition (and (web-agent ?agt) (reply-pending ?agt ?sid ?sent)) :effect (when (message-exchange ?agt ?sent ?received ?eff) ?eff))) O PT can be used purely as an ontology mechanism. We are working on using it as an internal notation for representation systems such as RDF [?, ?] and DAML [?], for which it provides type checking and other services. But the Lisp implementation of the O PT system, which is under con- struction, is the basis for support of various inferential systems, including a Prolog-style theorem prover, a planner [?], and a plan checker. The description of these systems and their APIs is beyond the scope of this manual, but will appear in later documentation. A formal semantics of O PT is in the works. In O PT, all types are capitalized, a style popularized by Java, and tending to create clarity in my opinion. In previous versions, PDDL has ignored case.1 O PT tools that offer a PDDL2.1- compatibility mode must also ignore it. 1 I think this was a bad design decision, even though I am largely responsible for it. However, in the future I would urge that this design decision be reversed, and that symbols which differ only in the case of some of their constituent characters be treated as different. 3 2 Technicalities Those not interested in technicalities may skip this section on first reading. As the example above shows: 1. The syntax of O PT is like Lisp’s. 2. Where types are declared, one does it by writing “ - type-expression” after the thing being declared. The details are fairly intricate and even interesting, but perhaps not right now. One other point: The enriched type system of O PT makes it possible to define many symbols simply by giving their types and a short definition, making it unnecessary to incorporate every symbol in a syntactic equation, as is the style in the various PDDL manuals. All symbols defined in this way are collected in section 13.3 in alphabetical order for easy reference. Furthermore, from this point on, every occurrence of such a symbol is flagged with a superscript •. so you won’t be baffled about where it is defined. Remember that upper-case symbols are types, and hence are documented in section 13.1; other symbols are documented in section 13.3. Requirements flags, which begin with a colon (“:”), are documented in section 13.2; because they are all built-in, their occurrences are not flagged. The only built-in constants that are not flagged are those with short, nonalphabetic names, such as +, =, <, and such, for which the annotation would be too distracting. 2.1 Syntactic Notation Our notation is the Extended BNF (EBNF) of [?] with the following conventions: • Each rule is of the form ::= expansion. • Angle brackets delimit names of syntactic elements. • Alternative expansions are written in two ways: by supplying two or more rules with the same left-hand side: ::= ( ∗) ::= (is ) or, if the alternative expansions are short, by writing one rule with the alternative expansions separated by “|”: ::= | • Square brackets ([ and ]) surround optional material. When a square bracket has a super- scripted requirement flag, such as: ...[:expansion ] :action−expansions 4 it means that the material is includable only if the domain being defined has declared a re- quirement for that flag. • Similarly, the symbol ::= may be superscripted with a requirement flag, indicating that the expansion is possible only if the domain has declared that flag. ::= :action−expansions • An asterisk (*) means “zero or more of”; a plus (+) means “one or more of.” • Some syntactic elements are parameterized. E.g., might denote a list of symbols, where there is an EBNF definition for and a definition for . The former might look like ::= (x *) so that a list of symbols is just (*). • Ordinary parenthesis are an essential part of the syntax we are defining; the only place they have a meaning in the EBNF meta language is inside angle brackets, where they wrap param- eters as just explained. Comments in O PT begin with a semicolon (“;”) and end with the next newline. Any such string behaves like a single space. Variables in OPT are always bound by explicit quantifiers or other devices. There is a tradition, in AI applications of logic, of flagging each occurrence of a variable somehow, by a prefix character (?x or :y, perhaps), or by a case convention (so that x is a variable and Xerxes is not, or vice versa). The original motivation for this convention was that variables were never declared, just implicitly universally quantified with scope equal to the largest formula they occurred in; so the occurrences had to be flagged. I find it odd that in formalisms with explicit declarations people still like those little reminders, which they cheerfully do without in programming languages and other contexts. In O PT, variables may be prefixed with question marks, but the question marks are almost always optional. The only exception is where the question mark is specifically for the purpose of avoiding an explicit declaration, as in the case of implicit type variables, discussed in section 2.2 2.2 The Type System The type system is ubiquitous in O PT. Intuitively, the type of an expression is a constraint on all the values the expression may ever have. To make this definition precise, we have to distinguish the type of an object from the type of an expression. An expression such as (+ x 3) will denote the number thirty-six in situations x where x denotes the number thirty-three. We write the names of the numbers out to emphasize that an object is drawn from an abstract universe of some kind, whereas an expression is drawn from a universe of lexical entities usually defined by recursive rules. The types of thirty-three and thirty-six are examples of object types; it happens that they are of type integer. Expression type is a useful concept only if it is used to reason about the types of the objects an expression will denote, i.e., its values, before it actually denotes them. In languages like Lisp and Kif, there is minimal use of expression type. Instead, every time the value of an expression 5 is available in a context where checking the appropriateness of that value is feasible, the run-time system can and usually does do the check, raising a run-time exception if the object fails the test. A classic example is evaluating (+ x 3) in an environment where the value of x is a string such as "oops", and getting an error message such as “Non-numerical argument "oops" to +.”2 It is harder to come up with examples in a declarative language such as Kif, because in the normal course of events expressions aren’t evaluated, but just used to infer further expressions. The consequence of a type error is likely to be a silent failure to draw an appropriate inference. O PT is also a declarative language. Long experience has taught us that detecting type errors before they occur saves a lot of debugging, and that requires figuring out the types of expressions, not objects. We declare the types of symbols, when they are first bound, by writing expression - type where the expression contains (and usually just is) the symbol. For instance, in a universally quan- tified statement we might say (forall (x - Vehicle) (has-gas-tank x)) to indicate that x ranges over Vehicles in this context. We follow the Java/Haskell convention of capitalizing the names of types. We do not follow the Java convention of usingCapitalLetters to indicateWordBoundaries; hyphens are treated as ordinary alphabetic characters, so we can write has-gas-tank instead of hasGasTank. The expression may be more complex. For instance, one construct for declaring a function looks, in part, like this example: (gcd i j - Integer •) - Integer • This declares the type of gcd, to wit, a function that takes two Integer arguments and produces an Integer result. Here we introduce the following terminological convention: In programming, if f is a function whose result type is y, we say f “returns” (an object of) type y. In logic, functions don’t get called, so they don’t actually “return” from anywhere. We will say instead that it produces type y. (Well, the truth is that for practical purposes we depart from this purity in “evaluation contexts”; see section 3.) Every expression must be typeable, meaning that it is possible to infer a consistent assignment of types to all its subexpressions, including itself. O PT does most of these inferences itself. It is often convenient to speak of “the type” of an expression, but this phrase is technically often wrong. An expression may have more than one type; typeability just means it is possible to find a consistent assignment of types of expressions. In the example, if has-gas-tank is a predicate on Physical-objects, and every Vehicle is a Physical-object, then the type of (has-gas-tank x) is Boolean 3. As this example 2 There is a philosophical problem here about the sense in which a computer can ever have access to the actual abstract universe of integers. The answer, of course, is that it can’t. It can, however, have access to a canonical representation of an abstract domain, including computable manipulations of that representation that provably correspond to or approximate actual mathematical functions on the abstract domain. Evaluating an expression E means finding the expression EC in the canonical representation that denotes the same object E does. A run-time type error corresponds to the detection of an E whose EC is not in the right subset of the canonical representation. 3 Actually, it’s not really Boolean, as we will discuss shortly. 6 shows, one type can be a subtype of another, as Vehicle is a subtype of Physical-object. Any term with type Vehicle also has type Physical-object. Types are not exactly sets; type theory is a competitor to set theory as a way of thinking about logic. In set theory, one starts with very general axioms about any kind of collection, and gradually infers theorems about various sorts of collection. In type theory, all the symbols (and compound expressions) must be labeled (or labelable) with their types. The labels must obey certain rules. For instance, if f is labeled as a function from String•s to Integer•s, then (f x) must be labeled Integer• and all occurrences of x must be labeled String•. A formula that cannot be given a type is ill-formed. In a sense the type of an expression identifies a set all its values fall in, but these sets are not first-class citizens in the logic. We can’t quantify over types; we can’t take intersection of types; we can’t infer that a type exists without knowing which type it is (i.e., knowing the standard name for it). In return for these constraints, it becomes easier to avoid paradoxes. The most famous paradox of set theory is Russell’s Paradox. Starting from the plausible idea that for any property there exists a set containing just the objects that satisfy that property, we quickly get a contradiction. For if the plausible idea is true, then from the property x !∈ x, we can derive the term S = {x|x !∈ x}. But then S ∈ S ⇐⇒ S !∈ S. Much ingenuity has been used in making this paradox go away. In type theory, it never arises, because terms x !∈ x and x ∈ x are not typeable. The type of ∈ is “predicate with two arguments, one an Individual, the other a Set.” To oversimplify x can be of type Individual or Set, but not both, so there is no way to infer a correct type for x ∈ x. We use a more Lisp-like notation. x ∈ x would be written (elt x x). The type of ∈, or elt, is (Fun Boolean <- (Individual Set)). (Fun range <- domain) is the type of functions from the given domain to the given range. The notation (Individual Set) is ac- tually short for (Arg• - Individual - Set), which describes an argument tuple with two anonymous elements (as indicated by the use of the name “ ”). Argument tuples are those evanescent entities that exist only when a function is called in Lisp. If you write (+ x y z), it is useful to analyze this as applying the function + to the argument tuple %x y z&, although this entity never exists as an actual data object (for instance, you can’t bind a variable to it). The basic rule for typing a function application is: If %a1 . . . ak & is an argument tuple with type A, and f has type (Fun r <- A), then (f a1 ... ak ) has type r. Function types are complicated by two phenomena: overloading and polymorphism. Overload- ing is the use of the same function symbol for different functions. The standard example is +, which can operate on Integer•s or Float•s. Fortunately, overloading is rare, and doesn’t require a general-purpose, user-level notation. In fact, the arithmetic functions are the only overloaded func- tions in O PT. Polymorphism is the use of a function symbol to denote a family of functions parameterized by one or more type variables. A standard example is the reverse function. If l is a list of objects, then (reverse l) is a list of the same elements, in the opposite order. It doesn’t matter what the types of the elements are, and they don’t all have to be the same type. One way to proceed is to declare reverse to be of type (Fun• (Lst• Obj• ) <- (Lst • Obj• )), where Obj• is a general type that includes all objects, and (Lst• y) is the type of lists of objects of type y. (We use the term type function for an entity such as Lst• that resembles a function syntactically, but produces a complex type from other types.) The problem is that if x is known to be of type (Lst• Integer •), we should be able to infer that (reverse x) is of the same type; but all we can infer is that (reverse x) is a list of Obj• . 7 What we want to do is introduce a type variable u and give reverse the type (Fun• (Lst• u) <- (Lst • u)). To avoid ambiguity about the scoping of u, we will actually declare reverse thus: reverse - (Fun • 1 (Fun• (Lst• u) <- (Lst • u)) <- (u - (T • ))) In other words, reverse is a function that takes u as an argument and produces a function type (Fun (Lst• u) <- (Lst • u)). The type of u is (T), meaning type. For example, (reverse Integer •) is a function of type (Fun (Lst• Integer •) <- (Lst • Integer •)). So one might expect to write ((reverse Integer•) x). We can’t actually do things quite that way, for a variety of reasons, including the fact that the first function application is obviously operating with “type-level” entities, while the second is operating with “domain-level” entities. The “1” in the first Fun signals this. Domain-level entities are at level 0, whereas type-level entities are at level 1. (The only level-2 entity in sight is the type (T), which is what type theorists call a kind, meaning that it is the type of a (level-1) type.) We indicate level-1 application with the symbol !&, so the proper way to write the example above is ((!& reverse Integer •) x) But this is too clumsy for the average case. We normally want to write simply (reverse x) We arrange for that with the following convention: If a level-1 function f is used where a level- 0 function is expected, say in the term (f a1 ...ak ), the type system will try to infer level-1 entities y1 . . . yn such that ((!& f y1 ...yn) a1 ...ak ) is typeable. If x is of type (Lst• Integer •), then the type system infers that (reverse x) means ((!& reverse Integer •) x), and is of type (Lst• Integer •). In addition, it is distracting to have to mention function levels in the usual case. Hence O PT allows some abbreviations. We can mush the two levels together reverse - (Fun (Lst • u) <- ((Lst • u) !& u - (T))) The label !& is used here to separate 0-level variables from 1-level variables. An alternative notation is to flag level-1 variables with question marks, as in reverse - (Fun (Lst • ?u) <- (Lst • ?u)) which is exactly equivalent to the original type declaration. This notation has the advantage of conciseness. It has the disadvantage that the scope of the variable ?u is not always clear. The rule is that the scope of a question-marked type variable is the outermost Fun such that the variable occurs in the type of one of its parameters. Using these notational devices, we can redo the Russell’s Paradox example in a more elegant way. Declare elt as follows: elt - (Fun Boolean <- (e - ?u s - (Set ?u))) 8 Here ?u is a level-1 variable, which can be any type. For any type t, there is a type of sets of t’s, which we denote by (Set t). Now (elt x x) is not typeable because there is no type u such that u = (Set u). Polymorphism has not been necessary for traditional planning applications, because the focus has been on manipulating simple objects. But for planning interactions with agents on the world- wide web, most actions include creating, and extracting data from, data structures. Here polymor- phism will be essential. However, it is hard to get interesting polymorphism without data structures such as (Lst• Integer •), and simple PDDL-style applications will not be able to handle them. Hence there is a requirement flag :data-structures that must be declared by any domain that uses them. In addition to Lst• , we have one other built-in complex type constructor: (Tup• –piece- declarations–) is a tuple with the given elements. Example: (Tup• i j - Integer • s - String •) is a tuple with three components, i, j, and s, of types Integer•, Integer •, and String •. Given a Tup• x, you can refer to the field named s by writing (! s x). If the fields are anonymous (named , in other words), you can refer to them positionally. The second element of u, where u - (Tup• - Integer •) can be accessed by writing (! <2> u). New type functions may be defined in terms of existing ones. See section 4. To refer to the object of a given type with given arguments, write (make type –arguments– ). For example, (make (Tup • i j - Integer •) 5 6) denotes a two-integer tuple x such that (! i x) is 5 and (! j x) is 6. This notation is not very useful without the ability to define named types, like this: In domain definition: (:type Int2 (Tup • i j - Integer •)) In some domain axiom: (list (make Int2 5 6) (make Int2 50 60)) The functions (list• a1 ...an ) and (tuple• a1 ...an) are a simpler way to make lists and tuples. The O PT system will try to infer the most useful type it can (either a Lst• or Tup• type) for an occurrence of one of these expressions. If y1 , . . . yl are types, then (Alt• y1 ...yl ) is the “union” of those types. An object is of this type if and only if it is of type yi for some i. For an expression to be of this type is for each of its possible values to be of type yi for some i. (A synonymous expression is (Either• y1 ... yl ).) We now describe the type-declaration notation using EBNF: ::= () ::= ∗ ::= + - ::= ::= ( +) ::= (Fun • [] <- ) ::= ( ) ::= ( ) 9 ::= ::= 0 | 1 ::= Tup • ::= | ::= | ([Arg] ) ::= | ([Arg] ) ::= [!& ] ::= [&optional ] [] ::= [!& ] ::= ∗ [&optional +] [] ::= | ::= &rest [- ] ::= &rest :- ::= &rest ( +) - ::= &key ::= | (( ) ) ::= &rest ::= &rest (= ) ::= &key (keytype) + ::= ::= | ( ) ::= ([Val] ∗) ([Val] ) ::= : ::= [?] ::= An EBNF definition of would be a bit clumsy; it’s easier just to say that a name is a sequence of one or more alphanumeric characters starting with an alphabetic. We count characters -, , +, -, *, /, <, and > as letters. (Note that colon is not allowed in a basic name. We will find a use for it in section 11.) A typed list is used to declare the types of a list of entities; the types are preceded by a hyphen (“-”), and every other element of the list is declared to be of the first type that follows it; if there are no types that follow it, O PT is to infer the type. An example of a is x y - Integer • ?l - (Lst • Integer •) 10 As explained above, the question marks in front of variables are optional. Fun• and Tup• are not quite type functions, because of their idiosyncratic syntax. The argu- ment position of a Fun• may be written (Arg• ...), or the Arg• may be implicit. Similarly, the value position of a Fun• may be written with or without the explicit Val• . The syntax of Arg• and Tup• are identical; Val is somewhat simpler. They are all based on the syntax of Common Lisp [?], which exploits fully parenthesized syntax to allow for very flexible argument-passing conventions. The easiest way to understand the Arg• syntax is to focus on the syntactic element ; is essentially the named version with the names re- moved. A specifies required arguments and optional arguments (if any), followed by either a &rest argument or a list of &key arguments. Every required argument is specified by a single named parameter. Optional arguments may have default values if omitted, in which case the parameter is written ( ). (The syntactic element will be explained in section 2.3.) If the default is not specified, it is the standard “zero” value for the parameter’s type (e.g., 0 for Integer•, "" for String •, and so forth). The &rest parameter row consists of a name followed by an optional type declaration. &rest m - Integer • indicates that the presence of zero or more Integer•s. In a Tup• , this notation means that the m slot (accessed by ! m) is of type (Lst• Integer •). A double hyphen is a variant in which we give the type of the slot rather than the type of each element of the slot. So we could write &rest m -- (Lst• Integer •) with the same meaning. Instead of a &rest parameter, one can write &key followed by a keyword parameters. In the simplest case parameters are declared as in this example: ff - (Fun • String• <- (&key x y - Integer •)) after which we can use ff by writing, e.g., (ff :x 3 :y 4), or (ff :y 40 :x 30), or even (ff :y 50). Keyword arguments may occur in any order, and some may be omitted. One can add a default value by writing a instead of a . One can make the keyword differ from the slot name by writing (( ) ). If we use these conventions to define ff, we might end up with: ff - (Fun • String• <- (&key (x -3) ((:y-arg y) 0) - Integer •)) So that (ff :y-arg 4) means the same as (ff :y 4 :x -3) in the previous version. If we declare a tuple thus: t1 - (Tup • &key (x -3) ((:y-arg y) 0) - Integer •) then if t1 is bound to the value of (tuple :y-arg 10), it will have two slots (! x t1), with value −3, and (! y t1), with value 10. There is one semantic difference between Tup• on the one hand, and Arg• and Val on the other. The latter are “row types,” meaning that an Arg• or a Val with one element is indistinguish- able from that element, whereas a tuple or record with one element is not the same as that element alone. A function whose range type is (Val n - Integer•) is the same as one with range type Integer •, except that the former allows us to use the name n to stand for the value in appropriate contexts. Type rows are essentially the same as parameter rows, but with all the names taken out. How- ever, we have to have conventions for handling nameless &rest and &key arguments. We interpret 11 &rest t as &rest - t; to say &rest -- t in parameterless style, write &rest (= t). For &key parameters, you simply write the keywords and their types. So the type of the second version of our function ff might be written (Fun• String• <- (&key (:x Integer •) (:y-arg Integer •))) For a table of all the built-in types of O PT, see section 13.1. 2.3 The Logical Language The basic syntax of the language is very simple. The primary syntactic element we define in this section is . Most terms are simple applications, of the form (f —args—). The term gram- mar is very general, and can generate lots of bogus terms, such as (+ (\\ (x) (1 x))). These terms are weeded out by the typeability requirement of section 2.2. As new syntactic constructs are presented, I will sketch the typeability rules associated with them. Let me emphasize again that the language I am describing is a logical language, not a program- ming language. To avoid misleading distractions I will eschew phrases like “the value of this term is . . . ,” and instead say things like “the denotation of this term is . . . .” To repeat what I said above, nothing is “called,” and nothing “returns a value” in a logical language. ::= | | ( +) ::= (!& +) ::= (make +) ::= ::= (! ) ::= (let-var [ :where )] ::= (\\ ) ::= (is ) ::= (be ) ::= (if ) ::= (-> ) ::= (<- ) ::= (when ) ::= (and ∗ ::= (or ∗) ::= (declare ) ::= ( ( []) ) ::= ( ) ::= [- ] ::= | | | ’ 12 ::= true | false ::= forall | exists | exists! | freevars Let’s explain each line in turn. The first line is self-explanatory. Literals in O PT include the usual Boolean•s, numbers (Integer• and Float•) and String•s, plus Symbol•s, which are just quoted names. (That is, there is a literal format for every primitive type in the hierarchy of section 3.) The second line, ::= ( +) is for function applications. A function application (f –arg tuple–) has type R if f has type (Fun• R <- A) and the arg tuple has type A. Note that the object in function position can be any term, not just a name, so long as it obeys this type rule. For instance, if m is of type (Lst• (Fun• String• <- Integer •)) then ((car m) 3) has type Integer •. ::= (!& +) refers to level-1 function application. The first term must denote a level-1 function. The arguments (if any) usually denote types, but other sorts of argument are allowed, provided they are all de- fined when the type of the term is determined. The typing rule for level-1 function application is essentially the same as the rule for level-0 application. ::= (! ) is for “slot access.” For this to be typeable, must be of a structured type (a Tup• ) with a field named . The term (! ) then refers to the contents of field . The type of the term is then the type of that field. If the structured type has anonymous fields, they can be referred to as if they were named <1>, <2>, etc. ::= (let-var () [ :where (] ::= ( ) The denotation of (let-var (–var-bindings–) e) is the denotation of e in an environment where each is bound to the denotation of its corresponding . If it’s clearer to put bindings at the end of the expression, you may do so, if they’re prefixed by keyword :where; the bindings at the front still have to be there, but can be (). Example: (let-var ((s (set-of-all (\\ (x - Planet) (inhabited x))))) (and (elt earth s) (elt mars s))) The type rule for (let-var ((v1 a1 ) ... (vk ak )) e) is that, if e has type t in an envi- ronment where each vi has type ti , where ti is the type of ai , then the entire let-expression has type t. 13 ::= (\\ ) ::= [- ] The \\ is our substitute for λ, which is not available on most keyboards. (\\ [- ] e) denotes an anonymous function whose arguments are given by the , and whose value, e, is of type . The value type is optional because O PT can usually figure it out. The typing rule for (\\ a e) is that if e has type t in an environment where all the variables of a have their declared types, then the \\ expression has type (Fun• t <- a). ::= (is ) (is t e) is true if and only if e is of the given type. This expression itself is of type Boolean. ::= (be ) is a declaration that the given is of the given type. You can abbreviate (! s (be t e)) as (! (t s) e). Note that be is merely a hint to the reader or the type checker that has the given type; it doesn’t override anything, or give rise to a “run-time check,” which is meaningless in a language with no run time. ::= (if ) has the usual meaning: (if v a b) has the same denotation as a if the denotation of v is true, and the same denotation as b if the denotation of v is false•. (if v a b) has type u if both a and b have type u. (if v a true) may be abbreviated (if v a). The variants (-> v a) and (<- a v) are explained in section 8. The variant (when v e) is explained in section 5.2. Some terms used in the antecedent (v-part) of an if have type implications. For instance, if we write (if (null l) 0 (- (car l))) in a context where l is declared to be of type (Lst• Number•), the fact that l is not empty, as it is known to be in the false branch of the if, implies that l is of type (Tup• Number• &rest Number •), and hence that (car l) is of type Number•. Similarly, in the true branch, l is known to be of type (Tup• ), the empty tuple. In general, we say that a term has type implications if knowing its type tells us something about the types of the variables that occur in it. (if w Bt Bf ) then really means (if w (declare I t B t) (declare I f B − f )) 14 where It are the type implications of knowing that w is of type (Con true• ) and If are the type implications of knowing that w is of type (Con false•). (See below for the explanation of declare.) Our example then translates to (if (null l) (declare (l - (Tup • )) 0) (declare (l - (Tup • Number• &rest Number •)) (- (car l)))) The connectives and and or are defined in terms of if in the usual way: (and) means true; (and c1 ...ck ) means (if c1 (and ...c k ) false•). (or) means false •; (or c1 ...ck ) means (if c1 true (or ...c k )). Because of these equivalences, and and or are not commutative, due to the possible type implications of ci on later cj . For example, (or (and (is Camel x) (two-hump x)) (and (is Rhino x) (one-horn x))) where two-hump and one-horn apply only to Camels and Rhinos, respectively, would not be typeable if the orders of the arguments to the ands were switched. The construct (is y x) has the obvious type implication, namely, that x is of type y. ::= (declare ) means the same thing as , except that hints are provided to the type checker that the vari- ables in should be treated as though they were of the declared types. Important: These hints cannot be used to change the types of the variables arbitrarily. If the type checker cannot prove that the variables have the indicated type, it should signal an error. [[Actually, it’s a bit more complicated than that. The type checker is allowed to constrain type variables in the course of the “proof,” so it’s more a license to discard some of the polymorphism. Example: if l is known to be of type “list of something,” (declare (l - (Lst• Eland)) ...) restricts it to be a list of Elands. ]] ::= ( ( []) ) There are four quantifiers, forall, exists, exists!, and freevars. (forall v P [v]) is true iff P [a] is true for all properly typed values of the variables in v. (exists v P [v]) is true iff P [a] is true for some value of the variables v. exists! is similar, but is true iff there is exactly one assignment to the variables v that makes P true. (freevars v P [v]) is a quantifier only “syntactically.” It just means, Let variables v be free in P [v], but it provides a way of declaring them. In most cases, freevars is synonymous with forall, as in Prolog. Quantified expressions are of type Prop, for “proposition.” The difference between a Prop and a Boolean is that the former can change value from situation to situation. For instance, 15 (location Titanic Southampton) is true in some situations, false, alas, in others. A Situation • is a state of affairs, a specification of the truth values of all ground atomic formulas. A Fluent • is a function from Situation•s to values; more precisely: Fluent • = (Fun• u <- (Situation • !& u)) We can then define a Prop as a (Fluent• Boolean). In most contexts, an object of type y is acceptable whenever an object of type (Fluent• y) is required, and vice versa. Appropriate coercion rules are applied, as described in section 3. For future reference in this manual, we introduce various subcategories of term, usually based on their types, but occasionally requiring other constraints. Here are some of those subcategories: • An is a term with type Action • A is a term with type Prop • A is a used to specify preconditions of ac- tions, and other goals. See section 5. • An is a used to specify effects of actions. See section 5.2. Let us close this section with a further exhortation not to assume that the logic subset of O PT is a programming language. When we write (if (> m n) m n), we do not mean, “Test whether m is greater than n, and if so. . . .” There may not be any method for testing the inequality, and if there is the agent may not always know it. When we write (exists (p - Planet) (and (orbits p sun) (not (= p earth)) (inhabited p))) we do not mean “Loop through the planets that orbit the sun.” Instead, the formula simply denotes true in universes where there is an inhabited planet in the solar system besides earth, and false• in all other universes. There may no easy way to tell which category our universe falls in. O PT does include an imperative sublanguage, which will be described in section 5. However, its semantics are completely compatible with the semantics of the rest of the language. That is, a term in the imperative sublanguage denotes something for an agent to do, sometimes a complex structure of actions. Considered as a term, that’s all it does. Of course, somewhere there has to be a plan executor that can take that term and perform the actions it describes. 3 Built-in Types: Primitives, Fluents, Expressions The primitive types, with subtype relationships shown, are as follows Obj Number Integer Float Char 16 String Symbol (These are all built in, and all described in section 13.3.) Arithmetic and comparison functions are defined on type Number•. However, the type-inference system treats these functions as overloaded, so that, for instance, if x is of type Float•, the ex- pression (+ x 1) is treated as meaning (+ x 1.0), and as being of type Float•. That is, an arithmetic expression is of type Integer• only if all its arguments are; if it has any argument of type Float•, it is of type Float•; otherwise, it is of type Number•. To make this work, O PT is provided with a modest coercion system that fixes type errors silently when it can using various ad-hoc rules. One of them is that if an Integer• is found where a Float• is wanted, the Integer• is treated as the Float• with the “same” value (in an inevitably implementation-defined sense). In addition, in domains declaring the :data-structures requirement, we have the type Sexp• , or “S-expression,” defined as (Alt• Symbol• String• Char• Number• (Lst• Sexp• ))) The type constructor (Fluent• y) is built in to O PT, and defined as (Fun• y <- Situation •), that is, a quantity of type y whose value changes from situation to situation. The type Prop• , for “proposition,” is the type produced by all predicates, and is defined as (Fluent• Boolean •). If a domain declares requirements :fluents, then there are many more possible things one can do with fluents, which will be described in the appropriate sections below. Arithmetic and comparison functions may, through the magic of coercion, be applied to fluents. Actually, the rule is more general. In any context where an expression of type y is wanted, if an expression e of type (Fluent• y) is found, it is treated as (fl-v• e), which means “the value of e in the current situation.” Similarly, if e is of type y, and (Fluent• y), is required, e is treated as (fl-∧• e), which means “the fluent that has value e in all situations.” If a domain declares requirement :expression-evaluation, then it supports computa- tional equality substitution, in which an expression such as (+ ?x 5) is replaced by 12 when ?x has value 7. The built-in predicate eval• provides the canonical context for this kind of substitu- tion: (eval• E V ) is true if the computational value of expression E is V . E is an expression using the functions +, -, *, /, min• , max• , and fl-v•. The first argument to e• val is said to be an evaluation context. If E contains any unbound variables, then it has no computational value, and no conclusion can be drawn regarding the truth or falsity of (eval• E V ). There are several other evaluation contexts in O PT, including both argument positions to the inequalities >, =<, etc. The proposition (bounded-int• I L H) is true if I is an integer in the interval [L, H]. L and H are evaluation contexts, as is I if it has no variables. Note that eval• is a special case of equality, with a nudge to the deductive system that its first argument should be evaluated. Another version of equality is (equation• L R), for which the “nudge” is as follows: If there is a single unbound deductive variable ?v with one or more occurrences in L and R, then for every value of x of that variable that makes the values of L and R the same, the conclude (= {v = x}(L) {v = x}(R)), where {v = x}(e) means e with all occurrences of ?v replaced with x. E.g., if ?y has been bound to 6, and ?x is unbound, then (equation (+ ?x 2) (- ?y 3)) is true, provided ?x = 1. Exactly what equations are 17 solvable is implementation-dependent, but every implementation should at least handle the case where there is a single occurrence of an unbound variable, buried at most inside an expression of the form (+/- ...). If the O PT syntax checker (which is beyond the scope of this manual) cannot figure out a valid type for an expression, it will issue an error message. Its complaints are usually correct, but some- times it has overlooked something. If you need to give it a hint about the type of an expression e, the usual way is to declare some of the variables occurring in e; an alternative is to replace e with (be y e) to declare that e should have type y. Then instead of trying to infer a type for e, it can work on the easier task of verifying the declared type. 4 Domains An Opt file consists of a series of domain definitions, addendum definitions, and problem definitions, defined here, in section 9, and section 10. The EBNF for defining a domain structure is: ::= (define (domain ) [] [] [] [] ∗ ∗ [] [] [] [] [] ∗) ::= (:extends +) ::= ::= See section 11. ::= See Section 11. ::= (:requirements +) ::= See Section 13.2 ::= (:types ) ::== (:type ) ::== (:type-fun ) ::= (:objects ) ::= (:parameters ) ::= (:predicates +) 18 ::= (:functions ) ::= ( ) ::= ( [- ] ) ::= (:facts +) ::= (:axioms +) ::= ::= :domain−axioms ::= :action−expansions ::= :processes ::= :durative−actions Although we have indicated the arguments in a particular order, they may come in any order, except for the (domain ...) itself. If the :extends argument is present, then this domain inherits requirements, types, objects, facts, axioms, and actions from the named domains, which are called the ancestors of this domain. Inheritance is transitive. The :requirements field is intended to formalize the fact that not all systems can handle all domains statable in the O PT notation. The listed requirements indicate the range of constructs that will be used in the domain being described. If a construct is used that requires a feature that the domain didn’t declare, an O PT processor should complain. In general, a domain is taken to declare every requirement that any ancestor declares. A description of all built-in requirements is found in Section 13.2. The defines simple named types. It uses a , but with a different interpretation than normal. (:types Elephant Ant - Animal Positive-integer - Integer •) declares three new types, Elephant, Ant, and Positive-integer, and declares them to be subtypes of Animal, Animal, and Integer •, respectively. (It does not declare any object to be any of those types.) A :type clause allows us to name an arbitrary type. Example: (:type Message (Lst • (Tup• String• String•))) This definition declares Message to be synonymous with (Lst• (Tup• String• String•)). By contrast, a :types clause declares a type to be an anonymous subtype of a given type. A :type-fun clause defines a type function. Example: (:type-fun (Mess a) (Lst• (Tup• a a))) The :parameters declaration is described in Section 3. The :objects field has the same syntax as the :types field, but the semantics is different. Now the names are taken as new constants in this domain, whose types are given as described above. E.g., the declaration 19 (:objects sahara - Theater division1 division2 - Division) indicates that in this domain there are three distinguished constants, sahara denoting a Theater and two symbols denoting Divisions. The :parameters field defines parameters that vary from domain to domain. [[These were originally called :domain-variables, but I believe “parameter” is a better term.]] The syntax is ::= (:parameters ) ::= | ( ) Each such parameter is treated as its value in evaluation contexts. E.g.: (define (domain cat-in-the-hat) (:types Thing - Integer) (:parameters (numthings 2) - Integer •) ... (:axiom :vars (?i - Integer •) :context (bounded-int • ?i 1 numthings) :implies (is Thing ?i))) The axiom (see section 8) states that “a Thing is an Integer between 1 and the value of numthings (in this domain, 2).” The :predicates field consists of a list of declarations of predicates, once again using the typed-list syntax to declare the arguments of each one. Example: (:predicates (loves ?x ?y - Person) (gender-of x - Person g - Gender)) The question marks before variables are optional in this context. The :functions field is a list of declarations of functions. A function f is a constructor of terms, (f --args--). It is not a function in the sense used in functional programming. To describe a function, we have to describe the types of its arguments, but also the type it produces. There are two places to put the type. One is after the function symbol, as in: (:functions (list-sum - Integer • (l - (Lst • Integer •))) (main-element - ?u (l - (Lst • ?u)))) indicating that list-sum produces type Integer•, and that main-element produces type ?u when given a list of objects of type ?u. The last question mark is significant; as explained in section 2.2, its presence declares main-element to be a level-1 function whose argument is a type u, and that produces a level-0 function that produces type u. Normally you may forget the details, unless your ontology fails to type-check. If several of the functions in the list produce the same type, we can move the type up a layer of parens: 20 (:functions (plus &rest l - Number •) (times &rest l - Number •) - Number • (book-title b - Book) (book-author b - Book) - String •) indicating that plus and times produce Number•, and book-title and book-author pro- duce String•.4 A predicate is just the special case of a function that produces type Prop. There is no difference between the :predicates declaration above and (:functions (loves ?x ?y - Person) (gender-of x - Person g - Gender) - Prop) The :facts field consists of a list of propositions that are taken to be true in this domain. (:axioms is treated as a synonym for :facts.) It goes without saying that the symbols used in the facts must be declared either here or in an ancestor domain. (Built-in predicates such as “=” behave as if they were inherited from an ancestor domain, although whether they actually are implemented this way depends on the implementation.) See section 8. A variable like this is scoped over the entire domain, and is inherited by domains that extend this one. If the variable is redeclared in an extending theory, it shadows the original binding. The remaining fields define actions and rules in the domain, and will be described in their own sections. 5 Actions 5.1 Syntax of Actions The EBNF for an action definition is: ::= (:action ( ) [ - ] ) :existential-preconditions ::= [] :conditional-effects [:precondition ] [:effect ] [:expansion ] :action−expansions [:only-in-expansions ] :action−expansions ::= :vars ::= :expansion 4 In PDDL2.1, functions all produce the type (Fluent Number). This design decision will surely be overturned as PDDL evolves, but implementations with a “PDDL2.1 compatibility mode” should provide (Fluent Number) as a default return type. 21 ::= :methods The preferred form for declaring the arguments and values of actions in O PT is to use parenthe- ses and hyphens in the same way that other functions are declared. However, it is also permissible to use the old-fashioned PDDL-style notation: ::= (:action :parameters [:value ] ) The :vars list are locally bound variables whose semantics are explained below. The :precondition is an optional goal proposition that must be satisfied for the action to be feasible. If no preconditions are specified, then the action is always feasible. The :effect field lists the changes which the action imposes on the current state of the world. A is a in which certain constructs are prohibited unless the domain declares certain requirements: Construct Requirement or, not, imply :disjunctive-preconditions exists* :existential-preconditions forall* :universal-preconditions The asterisks next to exists and forall are to remind us that an exists in a negative context should be treated as a forall, and vice versa. The polarity, positive or negative, of an occurrence of a subexpression is defined thus: Moving from the subexpression occurrence out- ward, count the number of nots encountered, plus the number of ifs that the occurrence oc- curs in the antecedent of. If the number is even, the subexpression is in a positive context; if odd, it’s in a negative context. So, if a domain declares :disjunctive-preconditions but not :universal-preconditions, then (not (exists (u v) ...)) is forbidden as a goal. If the domain declares requirement :action-expansions, then it is legitimate to include an :expansion field for an action, which specifies all the ways the action may be carried out in terms of (presumably simpler) actions. See Section 7. Free variables are not allowed. All variables in an action definition (i.e.,, in its precondition, ex- pansion, or effects) must be included in the :parameters, :vars, or :value list, or explicitly introduced with a quantifier. Variables appearing in the :vars field behave as if bound existentially in preconditions and universally in effects, except that it is an error if more than one instance satisfies the existential precondition. So, for example, in the following definition (:action spray-paint :parameters (?c - color) :vars (?x - location) 22 :precondition (at robot ?x) :effect (forall (?y - physob) (when (at ?y ?x) (color ?y ?c)))) the robot must be in at most one place to avoid an error. The optional argument :only-in-expansions is described in Section 7. 5.2 Effects and Values of Actions The effect of an action is the way the world changes as a result of executing the action. An has the syntax of a , but describes how the world is to change, not how it is, which is the usual meaning of a proposition. Hence we do not talk about the “truth value” of an effect proposition; it does not “become true,” but is imposed. There are certain pseudo- connectives allowed in this context that may not occur elsewhere, especially (when• p e), which means “If p was true just before the action was executed, then e (another effect proposition) is imposed as a result of its being executed.” In section 13.3, these pseudo-connectives, called effect predicates, are specially flagged. For the exact semantics of when• and its relatives, see section 6. Another pseudo-connective is not; (not p) is imposed by deleting p.5 In addition to an effect, the action may have a value, which reflects information acquired or created as a result of carrying out the action. For example, turning on a light in a dark room changes the average illumination level; it also tells you if there’s a hippopotamus in the room, which we can model by supposing the action returns an Integer• value: (:action (turn-on-light rm - Room) - (h - Integer •) :effect (and (bright rm) (not (dark rm)) (know-val-is (number-of-hippos rm) h))) The effect of (turn-on-light r) is that (bright r) becomes true and (dark r) becomes false. These effects then persist until the next action. The predicate (know-val-is t c), is supposed to be true if the agent knows that the value of term t is c, where c is a “computational” object (in this case, an Integer•). The :value field of an action specifies the type of the value returned when the action is per- formed. The value can be used as an input to a subsequent action by using a link, described in section 7. Even if it is not transmitted to another step, it can be referred to in the :effect field by declaring its fields and using them as if they were variables. In the example, h means “the ! h field of the value of this execution of (turn-on-light r).” Here’s another example (using the PDDL syntax): 5 It is surprisingly tricky to say what “deletion” is, but for domains not declaring the :open-world requirement, the idea is that every situation has a finite description as a list of atomic formulas; cf. section 10. The situation is obtained by assigning value true to formulas on the list, value false to all other atomic formulas, and then taking the deductive closure under all the axioms of the domain. Adding and deleting atomic formulas should be considered an operation on the finite description of the current situation; the resulting situation is then obtained by repeating the deductive-closure operation on the new finite description. For domains that do declare the :open-world requirement, the semantics of effects are murky and implementation-dependent. 23 (:action take-lunar-measurement :parameters () :precondition (...) :value (?az ?elv - Float •) :effect (and (know-val (azimuth moon) ?az) (know-val (elevation moon) ?elv))) As usual, the question marks are optional. An action definition defines a function; it takes arguments as specified in the , and produces an Action•. Actually, we can be more specific than that. If an action def- inition specifies no :expansion, then the action defined has type (Fun (Skip• r) <- a), where a and r are the argument type and result type specified in the definition. An object of type (Skip• r) is an action that takes one “instant” of time (in a sense explained in section 6) and re- turns a value of type r. I will call these skips. If an action definition does specify an :expansion, then its name is declared to be of type (Fun (Hop• r) <- a), as explained in more detail in sections 6.2 and 7. The type Skip-action• is defined to be (Skip• (Val• &rest Obj • )), that is, a skip that returns zero or more values. 5.3 Effects Involving Fluents If a domain declares requirement :fluents, then it supports some special predicates, particularly some new effect predicates. The effect predicate (assign F E) indicates that the value of fluent F changes to E. E is an evaluation context, and its value is computed with respect to the situation obtaining before the action (cf. when). The effect predicates (increase F E) and (decrease F E) are synonymous with (assign F (+ F E)) and (assign F (- F E)), respectively. Here is an example of how they are used: (:action (pour ?source ?dest - container) :vars (?sfl ?dfl - (fluent number) ?dcap - number) :precondition (and (contents ?source ?sfl) (contents ?dest ?dfl) (capacity ?dest ?dcap) (fluent-test (=< (+ ?sfl ?dfl) ?dcap))) :effect (and (assign ?sfl 0) (increase ?dfl ?sfl))) 6 Time and Processes 6.1 Process Syntax and Semantics If a domain declares requirement :processes, then it can have process definitions: ::= (:process( ) [- ] 24 ) :existential-preconditions ::= [] :conditional-effects [:condition ] [:start-effect ] [:effect ] [:stop-effect ] A process is like an action, except that it becomes active whenever its :condition is true, and remains active only for the time intervals over which the condition is true. The process is denoted by a constant term (name —args—), as described in its definition. The term names a unique process; there cannot be two distinct processes active at the same time named by the same term. Processes have three effects. To explain them, I have to explain, informally, a bit of the formal semantics of O PT. A situation is a snapshot of the state of the universe, i.e., a complete specification of the truth values of all logical formulas (which I will call “propositions” for brevity). The logical language of O PT is tenseless, so there are no formulas referring to the future or the past — and none referring to what time it is, although by using processes one can create clocks and hence get a time reading if you want.6 This semantic notion is distinct from the syntactic construct of section 10, although obviously the latter is meant to describe one of the former.7 In classical planning, situations occur in discrete chains, with instantaneous changes of the truth values of some propositions from one to the next. What happens in between is undefined, because there is no “in between.” Processes, however, can describe continuous changes. For instance, we might describe the process of water leaking from a can thus: (:process (leaking c - Can h - Hole) (:vars r - Float •) (:condition (and (hole-in h c) (>= (level c) (height h)) (= (rate-constant c) r))) (:effect (deriv-comp • (level c) (* r (- (level c) (height h)))))) In English: “If there is a hole h in can c, then so long as the water level stays above the height of h, the derivative of the level will have as one component an amount proportional to the difference between the water level and h’s height.” We use deriv-comp• here instead of derivative• because there may be other holes, plus other flows into the can, and it’s the job of the inference system, using a closed-world assumption, to infer what the net derivative is. 6 Although my semantic ideas borrow heavily from [?], this concept of situation is different from Reiter’s. He defines a situation in terms of the actions required to reach it. This is natural in some contexts, but in cases where a situation is not reachable by an agent’s action, or where we don’t care, and may not know, how a situation might have been reached, the analysis gets a bit strained. 7 And, as a previous footnote discusses, the semantics of not in action effects depends on the idea that every situation that occurs as the result of a chain of actions have a finite description using this syntax. 25 Obviously, the semantics of the leaking process can’t be described using discrete strings of situations. Instead we introduce the notion of a continuum of situations, in which an infinite number of situations can occur over a finite time period, during which quantities of type Float• can change continuously. Continuous and discrete changes have to be able to coexist. For instance, if there is an action puncture that makes holes in cans, a planner may introduce occurrences of it in order to speed up the emptying of a can. The most natural approach is to make puncture be a garden-variety, instantaneous, classical action. To allow for this, we use an idea from nonstandard analysis [?], per- mitting there to be an indefinite number of successors to a situation within an “infinitesimal” period of time. Formally, we model a situation continuum as a mapping from [0, ∞) × N to situations. The domain of this mapping is the set of ordered pairs %r, i&, where r is a real number ≥ 0 and i is an integer in the range [0, nr ]. The idea is that r is the date of the situation (measured in seconds from the initial situation), and i is the number of instantaneous planner actions that have occurred since r. The number nr is a function of the continuum, and is the number of instantaneous actions that actually occur at r in this continuum. If the planning agent does nothing, then nr = 0 for all r. At the points where it takes action, nr is the number of actions it takes (in sequence) at r. Following [?], we adopt the following constraint on action effects: In a given situation contin- uum, if an effect is imposed at point %r, nr &, then its changes must remain in place over an open interval in the continuum starting at r, that is, over an interval (r, r$ ), where r < r$ . We can then use the following semantic idea for when• and related constructs: (when• p e) is triggered at %r, i& if i = 0 and p is true over some open interval ending at r, or i > 0 and p is true at %r, i − 1&. If the when• is triggered, and i = nr then e is imposed over some open interval (closed on the left) starting at r; if i < nr , then e is imposed at %r, i + 1&. Real-world implementations of O PT can’t calculate the exact times when processes become active or inactive. They must find some close approximation instead. The domain parameter temporal-grain-size • provides a hint as to what “close” means. The value of this parameter, G, is a number representing a time interval such that any change in continuous quantities over an interval shorter than G is to be treated as negligible. Time is represented in seconds, so the de- 1 fault value, 0.01, of temporal-grain-size • means that changes over an interval less than 100 second are negligible. The parameter temporal-scope• is a time interval such that any event that far in the future is irrelevant. The default value is 1010 seconds, or about 3171 years. For every process P , there is a fluent (elapsed• P ) that is the time (in seconds) that P has been active. In situations where P is not active, (fl-v• (elapsed • P ))= −1. These fluents are updated automatically, and should not be altered by a user’s process or action definitions. Just as a skip-action name is of type (Fun (Skip• r) <- a) for some a and r, a process name is of type (Fun (Slide• r) <- a). The type Process • is defined to be (Slide• (Val• &rest Obj • )). It may seem odd to have processes “return” values, but there are cases, such as the autonomous action of an agent seeking information, where a return value makes sense. Such a value may be referred to in the :stop-effect field of a process definition just as an ordinary action’s value may be referred to in its :effect field. In addition, there is an action (wait-while• p) that waits for process p to end, then returns the same value p does. 26 6.2 Durative Actions Using the process formalism, it is possible to create models described by complex differential equa- tions, which are beyond the powers of almost all existing planning algorithms. In setting up the AIPS 2002 Planning Competition, it was desirable to find ways to constrain the formalism to make for solvable problems. A good way might have been to require all derivatives to be piecewise con- stant. Unfortunately, the way that was chosen was the somewhat odd notion of a “durative action,” an action that takes a certain amount of time. This idea may seem straightforward, when one thinks of examples like taking a plane from New York to Chicago, but even the straightforward examples start to break down if there is the slightest possibility that something might interfere with the ac- tion. In fact, in the cases where durative actions work, simple process models also work, so the advantages are not obvious. Nonetheless, as a public service, O PT includes durative actions. Here is the grammar: ::= (:durative-action ( ) [ - ] ) ::= :duration :condition :effect ::=:duration−inequalities (and +) ::= ::= ( ?duration ) ::= (at ) ::= = ::= :duration−inequalities =< | >=