idef3_kbsi_report (1013870), страница 39

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 39)

In the case of afunction, a complete definition provides a term that picks out the defined function. In the case ofa relation, a complete definition provides a set of sentences that jointly specify necessary andsufficient conditions for the relation being defined to hold. A partial definition puts constraintson the individual, function, or relation being defined that (in general) fall short of a full andcomplete definition. Partial definitions are frequently used simply to introduce a given term intothe language with no additional information. The operators:= and :=> are used in complete andpartial definitions, respectively.

In a complete individual definition, the name of the individualand a term defining the individual must be specified. In a partial definition, only the name of theindividual must be specified. Optionally, a sentence can be included in a partial definition torestrict the definition of the individual. A constant may have only one complete definition butseveral partial definitions.To illustrate, the function age-of and the individual Larry might be introduced by means ofthe following definitions.(define-function age-of(forall ?x (and (integer (age-of ?x)) (>= 0 (age-of ?x)))))(define-individual Larry(= (age-of Larry) 49).The optional sentence following the (partial) definition of “age-of” specifies that the indicatedfunction must return an integer greater than 0. This function is then used in the partial definitionof the term “Larry” to specify his age.Note that definitions can be used to explicitly introduce terms that denote functions andrelations equivalent to those denoted by lambda and kappa terms.

Thus, for instance, theproperty of being a person over 40 but under 60, referred to above by a kappa term, could benamed explicitly by an appropriate atomic term by means of the definition(define-relation middle-aged :=(and (person ?x) (> (age-of ?x) 40) (< (age-of ?x) 60)))).A.2BNF for the Elaboration Language CoreThis section contains the basic grammar for the elaboration language core in extendedBackus-Naur form (BNF). The following conventions are used:199A.2.1•A vertical bar “|” indicates an exclusive disjunction; thus C1 | C2 indicatesan occurrence of either C1 or C2, but not both. An absence of such a barindicates a conjunction.•A star “*” superscript immediately following a construct (e.g., C*) indicatesthat there can be zero, one, or more instances of a the construct.•A plus sign “+” superscript immediately following a construct (e.g., C+)indicates that there can be one or more instances of a the construct.•A construct or combination of constructs surrounded by brackets (e.g., [C1 |C2]) indicates that the construct or combination of constructs is optional.•In the following grammar, the terminals of the grammar—expressions thatare reserved in the elaboration language (i.e., that serve a particular purposein the language)—appear in bold face.

Nonterminals—expressionsrepresenting categories of expressions—start with "<" and end with ">". Forexample, the identifier for a variable must start with a question mark.Hence, the construct is shown as: <var> ::= ?<id>.AlphabetThe alphabet for the core of the elaboration language consists of the 93 ASCII characters withtheir standard print representations:ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789()[]{}<>=+-*/\&^~'`~"_@#$%:;,.!?The space character is represented by <space>.A.2.2Basic Syntactic Types<letter> ::=A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z<posdigit> ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9<digit> ::= 0 | <posdigit><id> ::= <letter> [[<letter> | <digit> | _ | -]* <letter> | [<letter> | <digit> | _ | -]* <digit>)]<punct> ::=_|-|~|!|@|#|$|%|^|&|*|(|)|+|=| `|:|;|'|<|>|,|.|?|/|||[|]|{|}<polarity> ::= + | –<posint> ::=<posdigit> <digit>+2000 | <posint><unsignedint> ::=<int>::=<unsignedint> | - <posint><exp>::=E <int> | e <int><float>::= <int><exp> |<int> .

<digit>+ [<exp>] |[+ | –] . <digit> <digit>* [<exp>]<number> ::=<int> | <float><string> ::= " [<letter> | <digit> | <punct> | <space> | \" | \\ ]* "<var>A.2.3::=?<id>Operators<operator> ::=<defop> | <termop> | <sentop><defop> :;=define-individual | define-function | define-relation | := | :=><termop> ::=number-of | if | cond | the<boolop> ::=not | and | or | xor | => | <=><quant> ::=forall | exists | exists[!]-<posint><sentop> ::=<boolop> | <quant>A.2.4Terms<term> ::= <atomterm> | <compterm><atomterm> ::= <id> | <var> | <int> | <float> | <string><compterm> ::= (<term> <term>+) |(if <sentence> <term> [<term>]) |(cond (<sentence> <term>) (<sentence> <term>)+) |(the <var> <sentence>) |(number-of <var> <sentence>) |(lambda <var> <term>) | (lambda (<var>+) <term>) |(kappa <var> <sentence>) | (kappa (<var>+) <sentence>)A.2.5Sentences<sentence> ::= <atomsent> | <boolsent> | <quantsent><atomsent> ::= (= <term> <term>) | (/= <term> <term>) | (<term> <term>+)201<boolsent> ::= (not <sentence>) | (and <sentence> <sentence>+) | (or <sentence> <sentence>+) |(xor <sentence> <sentence>+) | (=> <sentence> <sentence>) | (<=> <sentence><sentence>)<quantsent> ::= (<quant> <var> <sentence>]) |(forall (<var>+ [: <sentence>+]) <sentence>) |(exists (<var>+ [: <sentence>+]) <sentence>) |(exists[!]-<posint> (<var> : <sentence>) <sentence>)A.2.6Definitions<definition> ::= <partial-def> | <complete-def><complete-def> ::= (define-individual <id> := <term> ) |(define-function <id> (<var>+) := <term> ) |(define-relation <id> (<var>+) := <sentence> ) |<partial-def> ::= (define-individual <id> := <term> ) |(define-function <id> <sentence>*) |(define relation <id> (<var>*) :=> <sentence>)A.3Basic Definitions, Axioms, and Axiom SchemasThe syntax of the elaboration language is highly untyped; sentences and function terms arejust lists of terms with no enforced typing.

Instead, typing is enforced semantically, in the sensethat axioms are provided to ensure that an atomic sentence can be true, or a function term candenote a legitimate object, only if their constituent terms have the right sorts of denotations. Thisis accomplished by first introducing appropriate semantic categories (i.e., types) and auxiliarynotions by means of a series of “define-relation” and “define-function” statements, and thenaxiomatizing these notions to capture the relevant typing constraints. Note that these initialsemantic categories are completely general and independent of IDEF3. Only after these generalcategories are introduced and axiomatized are IDEF3-specific semantic categories and definitionsexplicitly introduced and axiomatized (see Section A.5).It should also be noted that some of the basic semantic categories of KIF, after which the coreelaboration language is modeled, are missing, most notably, sets and lists, which are notexplicitly needed for purposes here.

Strictly speaking, set theory is needed to justify definitions,as one must (or at least ought to) be able to prove the existence of the objects one defines (exceptin the case where one is simply postulating or introducing an object whose existence cannot beproved from one’s given axioms). Their omission here reflects the idea that users should havethe option to choose their own set theories; in particular, a user might wish to use one weakerthan the powerful von Neumann-Gödel-Bernays set theory of KIF. While acknowledging theneed for an associated set theory, commitment to a given set theory is left implicit in this report.202A.3.1Basic Semantic CategoriesIn this section, the basic semantic categories individual, function, and relation are introduced,as well as the null object, a special object used only to indicate that a term has no genuinedenotation.(define-relation individual (?x))(define-relation list (?x))(define-relation relation (?x))(define-individual null)(define-relation function (?x)):=> (relation ?x))(define-relation interval (?x):=> (individual ?x))(define-relation integer (?x):=> (individual ?x))Most formalizations involving functions define functions as relations of a certain sort.

Характеристики

Список файлов учебной работы