Misplaced Pages

#184815

54-489: RIF includes three dialects, a Core dialect which is extended into a Basic Logic Dialect (BLD) and Production Rule Dialect (PRD). The RIF working group was chartered in late 2005. Among its goals was drawing in members of the commercial rules marketplace. The working group started with more than 50 members and two chairs drawn from industry, Christian de Sainte Marie of ILOG , and Chris Welty of IBM . The charter, to develop an interchange format between existing rule systems

108-527: A l s e ⟨ w h i l e   B   d o   C , s ⟩ ⟶ s {\displaystyle {\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}} Such

162-560: A C# version of some of its visualization products in fiscal year 2004 and of their BRMS products in fiscal year 2005. Until ILOG's initial public offering in 1997 on the NASDAQ National Market (which subsequently became the Nasdaq Stock Market on August 1, 2006), ILOG was financed through a combination of retained earnings, venture capital funding and interest free loans from French government agencies and

216-413: A Curry-Feys standardization lemma for the transitive-reflexive closure of the single-step relation, which replaces the non-deterministic search in the evaluation function with a deterministic left-most/outermost search. Felleisen showed that imperative extensions of this calculus satisfy these theorems. Consequences of these theorems are that the equational theory—the symmetric-transitive-reflexive closure—is

270-851: A PARLE 1987 paper. Reduction semantics are given as a set of reduction rules that each specify a single potential reduction step. For example, the following reduction rule states that an assignment statement can be reduced if it sits immediately beside its variable declaration: l e t   r e c   x = v 1   i n   x ← v 2 ;   e     ⟶     l e t   r e c   x = v 2   i n   e {\displaystyle \mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e} To get an assignment statement into such

324-429: A business rule management system (BRMS) product in 1996, which gives software engineers the ability to better manage the rules operating their applications. The financial services sector has been the primary market for ILOG's BRMS products, for use in developing, for example, online trading or credit decision making applications. ILOG's BRMS product line is currently the company's largest product line. ILOG also introduced

378-423: A definition allows formal analysis of the behavior of programs, permitting the study of relations between programs. Important relations include simulation preorders and bisimulation . These are especially useful in the context of concurrency theory . Thanks to its intuitive look and easy-to-follow structure, SOS has gained great popularity and has become a de facto standard in defining operational semantics. As

432-777: A direct representation of uncertain knowledge. Example: RIF-SILK can be used to model default logic . It is based on declarative logic programming with the well-founded semantics . RIF-SILK also includes a number of other features present in more sophisticated declarative logic programming languages such as SILK. Example ILOG ILOG S.A. was an international software company purchased and incorporated into IBM announced in January, 2009. It created enterprise software products for supply chain , business rule management, visualization and optimization. The main product line for Business Rules Management Systems (BRMS) has been rebranded as IBM Operational Decision Management . Many of

486-476: A number of distinctions between small-step and big-step semantics that influence whether one or the other forms a more suitable basis for specifying the semantics of a programming language. Big-step semantics have the advantage of often being simpler (needing fewer inference rules) and often directly correspond to an efficient implementation of an interpreter for the language (hence Kahn calling them "natural".) Both can lead to simpler proofs, for example when proving

540-481: A popular choice for semantics specification in programming languages, but it has some drawbacks that make it inconvenient or impossible to use in many situations, such as languages with control-intensive features or concurrency. A big-step semantics describes in a divide-and-conquer manner how final evaluation results of language constructs can be obtained by combining the evaluation results of their syntactic counterparts (subexpressions, substatements, etc.). There are

594-487: A position it is “bubbled up” through function applications and the right-hand side of assignment statements until it reaches the proper point. Since intervening l e t {\displaystyle \mathbf {let} } expressions may declare distinct variables, the calculus also demands an extrusion rule for l e t {\displaystyle \mathbf {let} } expressions. Most published uses of reduction semantics define such “bubble rules” with

SECTION 10

#1732780131185

648-535: A sign of success, the original report (so-called Aarhus report) on SOS ( Plotkin81 ) has attracted more than 1000 citations according to the CiteSeer [1] , making it one of the most cited technical reports in Computer Science . Reduction semantics is an alternative presentation of operational semantics. Its key ideas were first applied to purely functional call by name and call by value variants of

702-675: A sound reasoning principle for these languages. However, in practice, most applications of reduction semantics dispense with the calculus and use the standard reduction only (and the evaluator that can be derived from it). Reduction semantics are particularly useful given the ease by which evaluation contexts can model state or unusual control constructs (e.g., first-class continuations ). In addition, reduction semantics have been used to model object-oriented languages, contract systems , exceptions, futures, call-by-need, and many other language features. A thorough, modern treatment of reduction semantics that discusses several such applications at length

756-585: A term is plugged in a capturing fashion. The shape of the context indicates with this hole where reduction may occur. To describe “bubbling” with the aid of evaluation contexts, a single axiom suffices: E [ x ← v ;   e ]     ⟶     x ← v ;   E [ e ] (lift assignments) {\displaystyle E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}} This single reduction rule

810-439: A valid program is interpreted as sequences of computational steps. These sequences then are the meaning of the program. In the context of functional programming , the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could be nondeterministic , and even for a deterministic program there can be many computation sequences since

864-482: Is a category of formal programming language semantics in which certain desired properties of a program , such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms ( denotational semantics ). Operational semantics are classified in two categories: structural operational semantics (or small-step semantics ) formally describe how

918-462: Is a quote from the revised ALGOL 68 report: The meaning of a program in the strict language is explained in terms of a hypothetical computer which performs the set of actions that constitute the elaboration of that program. ( Algol68 , Section 2) The first use of the term "operational semantics" in its present meaning is attributed to Dana Scott ( Plotkin04 ). What follows is a quote from Scott's seminal paper on formal semantics, in which he mentions

972-405: Is an abbreviation of the combination of two French words: "Intelligence" and "Logiciel". These words can be translated as "Intelligent Software." In 1987, ILOG began licensing software components to companies developing software applications. These customers licensed the components in order to add new functionality to their software applications. The software components were initially developed in

1026-453: Is checkable in some dataset holds, then the conclusion (the THEN part) is processed. Deriving somewhat from its roots in logic , rule systems use a notion of predicates that hold or not of some data object or objects. For example, the fact that two people are married might be represented with predicates as: MARRIED is a predicate that can be said to hold between LISA and JOHN . Adding

1080-667: Is given by Matthias Felleisen, Robert Bruce Findler and Matthew Flatt in Semantics Engineering with PLT Redex . Big-step structural operational semantics is also known under the names natural semantics , relational semantics and evaluation semantics . Big-step operational semantics was introduced under the name natural semantics by Gilles Kahn when presenting Mini-ML, a pure dialect of ML . One can view big-step definitions as definitions of functions, or more generally of relations, interpreting each language construct in an appropriate domain. Its intuitiveness makes it

1134-424: Is just the first part of a program.") The semantics is structural, because the meaning of the sequential program C 1 ; C 2 {\displaystyle C_{1};C_{2}} , is defined by the meaning of C 1 {\displaystyle C_{1}} and the meaning of C 2 {\displaystyle C_{2}} . If we also have Boolean expressions over

SECTION 20

#1732780131185

1188-480: Is not a logic-based RIF dialect. The Basic Logic Dialect (BLD) adds features to the Core dialect that are not directly available such as: logic functions, equality in the then-part and named arguments . RIF BLD corresponds to positive datalogs, that is, logic programs without functions or negations. RIF-BLD has a model-theoretic semantics. The frame syntax of RIF BLD is based on F-logic , but RIF BLD doesn't have

1242-456: Is relatively easy to implement inference engines that can process the conditions and draw the right conclusions. A rule system is an implementation of a particular syntax and semantics of rules, which may extend the simple notion described above to include existential quantification , disjunction , logical conjunction , negation , functions , non monotonicity , and many other features. Rule systems have been implemented and studied since

1296-418: Is the lift rule from Felleisen and Hieb's lambda calculus for assignment statements. The evaluation contexts restrict this rule to certain terms, but it is freely applicable in any term, including under lambdas. Following Plotkin, showing the usefulness of a calculus derived from a set of reduction rules demands (1) a Church-Rosser lemma for the single-step relation, which induces an evaluation function, and (2)

1350-587: The company started to expand globally by establishing a major sales presence in the United States and Asia. In 1997 Apr 19, it acquired CPLEX Optimization, Inc. (CPLEX), located in Incline Village, Nevada, which provided linear-based optimization software products for the supply chain industry. In the late 1990s, ILOG started to introduce Java versions of its products to follow once again the software industry’s technical evolution. It also introduced

1404-414: The individual steps of a computation take place in a computer-based system; by opposition natural semantics (or big-step semantics ) describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics . The operational semantics for a programming language describes how

1458-418: The lambda calculus by Gordon Plotkin in 1975 and generalized to higher-order functional languages with imperative features by Matthias Felleisen in his 1987 dissertation. The method was further elaborated by Matthias Felleisen and Robert Hieb in 1992 into a fully equational theory for control and state . The phrase “reduction semantics” itself was first coined by Felleisen and Daniel P. Friedman in

1512-554: The non-monotonic reasoning features of F-logic. The Production Rules Dialect (PRD) can be used to model production rules . Features that are notably in PRD but not BLD include negation and retraction of facts (thus, PRD is not monotonic). PRD rules are order dependent, hence conflict resolution strategies are needed when multiple rules can be fired. The PRD specification defines one such resolution strategy based on forward chaining reasoning. RIF-PRD has an operational semantics , whereas

1566-688: The "Transfer of Business" letter was issued that confirmed that ILOG was effectively integrated within IBM . This coincided with a fresh release of the ILOG products, which is now branded as an IBM ILOG company. As of 2009, more than 1,000 universities use ILOG Optimization for research and teaching, and more than 1,000 commercial customers, including over 160 of the Global 500, use ILOG Optimization in some of their most important planning and scheduling applications. Operational semantics Operational semantics

1620-519: The "operational" aspects of semantics. It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach to semantics, but if the plan is to be any good, the operational aspects cannot be completely ignored. ( Scott70 ) Gordon Plotkin introduced the structural operational semantics, Matthias Felleisen and Robert Hieb the reduction semantics, and Gilles Kahn the natural semantics. Structural operational semantics (SOS, also called structured operational semantics or small-step semantics )

1674-606: The European Union. This initial public offering enabled ILOG to acquire CPLEX. In 1998, SAP A.G. invested in ILOG. The financing from SAP was part of the partnership that has made SAP ILOG's biggest customer every year to date. This partnership, along with others, made ILOG a player in the supply chain management market. In 1998, ILOG listed on the Nouveau marché of Euronext Paris and in 2005 transferred to Eurolist by Euronext Paris. On October 26, 2006, ILOG acquired 35% of

Rule Interchange Format - Misplaced Pages Continue

1728-558: The LISP programming language, and transitioned to C++ in 1992 in order to follow the technical evolution of the software industry. ILOG introduced two new products in 1993: ILOG Views and ILOG Solver. ILOG customers use them to make visualization interfaces (Views) and resources allocation applications (Solver). Until 1995, ILOG sales were concentrated in Europe, particularly in France. In 1995,

1782-881: The United Kingdom. Through its acquisition of CPLEX Optimization Inc. in 1997, ILOG became the owner of the CPLEX mathematical programming software, and ILOG's acquisition of LogicTools in 2007 made ILOG the owner of a line of supply chain applications. The CPLEX and other tools also had some minor rebranding under the IBM Optimization Suite of tools. ILOG's main products: ILOG was an international software company. It developed, marketed, sold and supported BRMS, optimization and visualization software components, as well as supply chain applications. ILOG had business locations in nine countries, but it had two principal locations incorporated into IBM: The name ILOG

1836-485: The acquisition of LogicTools , a Chicago-based provider of supply chain planning applications specializing in network design and inventory optimization . LogicTools’ applications are based on the ILOG CPLEX optimization product. On July 28, 2008, IBM and ILOG announced an agreement regarding a proposed acquisition by IBM of ILOG. On January 6, 2009, the acquisition of ILOG by IBM was completed. On July 1, 2009,

1890-486: The capital and voting rights of the Chinese company Shanghai FirstTech Co., Ltd. (FirstTech). FirstTech is a systems integrator that develops and markets manufacturing and insurance solutions in the Chinese market. On November 20, 2006, ILOG acquired one-third of the capital and voting rights of Prima Solutions (Prima), a Paris-based supplier of software platforms for the insurance sector. On April 11, 2007, ILOG completed

1944-512: The condition formulas also have a model-theoretic semantics. Example (Example 1.2 in ) Several other RIF dialects exist. None of them are officially endorsed by W3C and they are not part of the RIF specification. The Core Answer Set Programming Dialect (CASPD) is based on answer set programming , that is, declarative logic programming based on the answer set semantics ( stable model semantics ). Example: The Uncertainty Rule Dialect (URD) supports

1998-984: The convenience of evaluation contexts. For example, the grammar of evaluation contexts in a simple call by value language can be given as E ::= [ ]   |   v   E   |   E   e   |   x ← E   |   l e t   r e c   x = v   i n   E   |   E ;   e {\displaystyle E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e} where e {\displaystyle e} denotes arbitrary expressions and v {\displaystyle v} denotes fully-reduced values. Each evaluation context includes exactly one hole [ ] {\displaystyle [\,]} into which

2052-455: The datatypes are adapted from XML Schema Datatypes, XPath functions and rdf:PlainLiteral functions. The Core dialect comprises a common subset of most rule dialect. RIF-Core is a subset of both RIF-BLD and RIF-PRD. Framework for Logic Dialects (FLD) describes mechanisms for specifying the syntax and semantics of logic RIF dialects, including the RIF-BLD and RIF-Core, but not RIF-PRD which

2106-415: The first rule says that, if program C 1 {\displaystyle C_{1}} in state s {\displaystyle s} finishes in state s ′ {\displaystyle s'} , then the program C 1 ; C 2 {\displaystyle C_{1};C_{2}} in state s {\displaystyle s} will reduce to

2160-1178: The following three rules: ⟨ C 1 , s ⟩ ⟶ s ′ ⟨ C 1 ; C 2 , s ⟩ ⟶ ⟨ C 2 , s ′ ⟩ ⟨ C 1 , s ⟩ ⟶ ⟨ C 1 ′ , s ′ ⟩ ⟨ C 1 ; C 2 , s ⟩ ⟶ ⟨ C 1 ′ ; C 2 , s ′ ⟩ ⟨ s k i p , s ⟩ ⟶ s {\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}} Informally,

2214-502: The form of a set of inference rules that define the valid transitions of a composite piece of syntax in terms of the transitions of its components. For a simple example, we consider part of the semantics of a simple programming language; proper illustrations are given in Plotkin81 and Hennessy90 , and other textbooks. Let C 1 , C 2 {\displaystyle C_{1},C_{2}} range over programs of

Rule Interchange Format - Misplaced Pages Continue

2268-762: The language, and let s {\displaystyle s} range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by E {\displaystyle E} ), values ( V {\displaystyle V} ) and locations ( L {\displaystyle L} ), then a memory update command would have semantics: ⟨ E , s ⟩ ⇒ V ⟨ L := E , s ⟩ ⟶ ( s ⊎ ( L ↦ V ) ) {\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}} Informally,

2322-501: The mid-1970s and saw significant uptake in the 1980s during the height of so-called Expert Systems . The standard RIF dialects are Core, BLD and PRD. These dialects depend on an extensive list of datatypes with builtin functions and predicates on those datatypes. Relations of various RIF dialects are shown in the following Venn diagram. Datatypes and Built-Ins (DTB) specifies a list of datatypes, built-in functions and built-in predicates expected to be supported by RIF dialects. Some of

2376-520: The notion of variables, a rule could be something like: We would expect that for every pair of ?x and ?y (e.g. LISA and JOHN ) for which the MARRIED predicate holds, some computer system that could understand this rule would conclude that the LOVES predicate holds for that pair as well. Rules are a simple way of encoding knowledge, and are a drastic simplification of first order logic , for which it

2430-420: The preservation of correctness under some program transformation . The main disadvantage of big-step semantics is that non-terminating ( diverging ) computations do not have an inference tree, making it impossible to state and prove properties about such computations. Small-step semantics give more control over the details and order of evaluation. In the case of instrumented operational semantics, this allows

2484-485: The program C 1 {\displaystyle C_{1}} in state s {\displaystyle s} can reduce to the program C 1 ′ {\displaystyle C_{1}'} with state s ′ {\displaystyle s'} , then the program C 1 ; C 2 {\displaystyle C_{1};C_{2}} in state s {\displaystyle s} will reduce to

2538-400: The program C 1 ′ ; C 2 {\displaystyle C_{1}';C_{2}} in state s ′ {\displaystyle s'} . (You can think of this as formalizing the principle for an optimizing compiler: "You are allowed to transform C 1 {\displaystyle C_{1}} as if it were stand-alone, even if it

2592-402: The program C 2 {\displaystyle C_{2}} in state s ′ {\displaystyle s'} . (You can think of this as formalizing "You can run C 1 {\displaystyle C_{1}} , and then run C 2 {\displaystyle C_{2}} using the resulting memory store.) The second rule says that if

2646-608: The related components retain the ILOG brand as a part of their name. The software developed by the ILOG software company supports several software platforms, including COBOL , C++ , C# , .NET , Java , AJAX and Adobe Flex and Flex AIR. Founded in 1987 in Paris , France, ILOG had its main headquarters in Gentilly , France, and Sunnyvale , California. It also had main offices in Australia, China, Germany, Japan, Singapore and

2700-477: The rule says that " if the expression E {\displaystyle E} in state s {\displaystyle s} reduces to value V {\displaystyle V} , then the program L := E {\displaystyle L:=E} will update the state s {\displaystyle s} with the assignment L = V {\displaystyle L=V} ". The semantics of sequencing can be given by

2754-493: The semantics may not specify exactly what sequence of operations arrives at that value.) Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of Lisp . Abstract machines in the tradition of the SECD machine are also closely related. The concept of operational semantics was used for the first time in defining the semantics of Algol 68 . The following statement

SECTION 50

#1732780131185

2808-560: The state, ranged over by B {\displaystyle B} , then we can define the semantics of the while command: ⟨ B , s ⟩ ⇒ t r u e ⟨ w h i l e   B   d o   C , s ⟩ ⟶ ⟨ C ; w h i l e   B   d o   C , s ⟩ ⟨ B , s ⟩ ⇒ f

2862-461: Was influenced by a workshop in the spring of 2005 in which it was clear that one rule language would not serve the needs of all interested parties (Dr. Welty described the outcome of the workshop as Nash Equilibrium ). RIF became a W3C Recommendation on June 22, 2010. A rule is perhaps one of the simplest notions in computer science: it is an IF - THEN construct. If some condition (the IF part) that

2916-434: Was introduced by Gordon Plotkin in ( Plotkin81 ) as a logical means to define operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax-oriented and inductive , view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) transition relation (s). SOS specifications take

#184815