RE: DTB and BLD Use Cases: User-Defined Functions -- factorial example, Equal in the head, oriented equations, left and right roles

Hi RIF WG,

Here's the current XML syntax (with proposed differentiation
of <side> into <left> and <right> indicated as XML comments):


<?xml version="1.0" encoding="UTF-8"?>

<!--

Example of equational factorial function definition

-->

<!DOCTYPE Document [
  <!ENTITY rif "http://www.w3.org/2007/rif#">
  <!ENTITY pred "http://www.w3.org/2007/rif-builtin-predicate#">
  <!ENTITY func "http://www.w3.org/2007/rif-builtin-function#">
  <!ENTITY xsd "http://www.w3.org/2001/XMLSchema#">
]>
  
<Document 
    xmlns="http://www.w3.org/2007/rif#"
    xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
    xmlns:xs="http://www.w3.org/2001/XMLSchema#">
  <payload>
   <Group>
    <sentence>
     <Equal>
       <side> <!-- <left> -->
         <Expr>
           <op><Const type="&rif;local">factorial</Const></op>
           <args ordered="yes"><Const
type="&xsd;integer">0</Const></args>
         </Expr>
       </side> <!-- </left> -->
       <side><Const type="&xsd;integer">1</Const></side>  <!-- <right>
... </right> -->
     </Equal>
    </sentence>
    <sentence>
     <Forall>
       <declare><Var>N</Var></declare>
       <formula>
         <Implies>
           <if>
             <Atom>
               <op><Const
type="&rif;iri">&pred;numeric-greater-than</Const></op>
               <args ordered="yes">
                 <Var>N</Var>
                 <Const type="&xsd;integer">0</Const>
               </args>
             </Atom>
           </if>
           <then>
             <Equal>
               <side> <!-- <left> -->
                 <Expr>
                   <op><Const type="&rif;local">factorial</Const></op>
                   <args ordered="yes"><Var>N</Var></args>
                 </Expr>
               </side> <!-- </left> -->
               <side> <!-- <right> -->
                  <Expr>
                     <op><Const
type="&rif;iri">&func;numeric-multiply</Const></op>
                     <args ordered="yes">
                       <Var>N</Var>
                       <Expr>
                         <op><Const
type="&rif;local">factorial</Const></op>
                         <args ordered="yes">
                           <Expr>
                             <op><Const
type="&rif;iri">&func;numeric-subtract</Const></op>
                             <args ordered="yes">
                               <Var>N</Var>
                               <Const type="&xsd;integer">1</Const>
                             </args>
                           </Expr>
                         </args>
                       </Expr>
                     </args>
                  </Expr>
               </side> <!-- </right> -->
             </Equal>
           </then>
         </Implies>
       </formula>
     </Forall>
    </sentence>
   </Group>
  </payload>
 </Document>


You can validate this factorial.rif example _online_ at
http://www.w3.org/2005/rules/wiki/BLD#Appendix:_XML_Schema_for_RIF-BLD

Best,
Harold


-----Original Message-----
From: Boley, Harold 
Sent: June 10, 2008 12:04 PM
To: 'Public-Rif-Wg (E-mail)'
Subject: DTB and BLD Use Cases: User-Defined Functions -- factorial
example, Equal in the head, oriented equations, left and right roles

Hi RIF WG,

User-defined functions on top of the DTB built-ins
will make for some interesting Use Cases. These can
lead to a better understanding of our work so far.

For example, the factorial function can be defined
in BLD presentation syntax based on DTB built-ins:

Document(

  Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
  Prefix(func http://www.w3.org/2007/rif-builtin-function#)

  Group
  (
    factorial(0) = 1

    Forall ?N (
      factorial(?N) = func:numeric-multiply
                       (?N
                        factorial(func:numeric-subtract(?N 1)))
        :- pred:numeric-greater-than(?N 0)
    )
  )
)

Both Equals are oriented/directed from left to right here,
as often occurs in practice (so I think we should use
selective <side> roles, <left> and <right>, within <Equal>).
The Equal is the stand-alone head/conclusion of the base fact
and the head of the recursive rule (so I would 'lower' the
"at risk" of Equal-in-the-head for oriented equations).

Best,
Harold

Received on Wednesday, 11 June 2008 23:03:21 UTC