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

<?xml-model href="http://www.ruleml.org/1.0/relaxng/hornlogeq_relaxed.rnc"?>
<!--<?xml-model href="http://www.ruleml.org/1.0/xsd/hornogeq.xsd" type="application/xml" schematypens="http://www.w3.org/2001/XMLSchema"?>-->
<!--<RuleML xmlns="http://ruleml.org/spec"
  xmlns:xs="http://www.w3.org/2001/XMLSchema"
  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
  xsi:schemaLocation="http://ruleml.org/spec http://www.ruleml.org/1.0/xsd/naffologeq.xsd"> -->

<RuleML xmlns="http://ruleml.org/spec"
  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
  xmlns:xs="http://www.w3.org/2001/XMLSchema">

  <Assert node="#KB1">
    <!-- A Knowledge Base with some function definitions. -->
    <Equal>
      <Expr>
        <Fun per="value">f</Fun>
        <Ind>a</Ind>
      </Expr>
      <Data xsi:type="xs:integer">4</Data>
    </Equal>
    <Equal>
      <Expr>
        <Fun per="value">f</Fun>
        <Data xsi:type="xs:integer">4</Data>
      </Expr>
      <Data xsi:type="xs:integer">16</Data>
    </Equal>
  </Assert>

  <Query>
    <!-- Substitution of the values of constants (<Ind>) or expressions (<Expr>) 
         is not allowed in reification, even if the expression has @per="value".
         However, variables (<Var>) inside a reification may be replaced with values,
         including RuleML fragments.
         When such substitution is possible, it is often referred to as "referential transparency".
         Using this terminology, <Reify> is only referentially transparent for variables.-->
    <Equal>
      <Reify>
        <Expr>
          <Fun per="value">f</Fun>
          <Ind>a</Ind>
        </Expr>
      </Reify>
      <Var>X</Var>
    </Equal>
  </Query>
  <!-- 
  Result    
      Success
  
  Variable
      <Var>X</Var>
  
  Values   
  <Reify>  
    <Expr>
      <Fun per="value">f</Fun>
      <Ind>a</Ind>
    </Expr>
  </Reify>  
  -->

  <Query>
    <!-- For comparison, a query of the knowledge base asserted above (<Ind>KB1</Ind>)
         using an unreifed expression with per="value" is evaluated. -->
    <Equal>
      <Expr>
        <Fun per="value">f</Fun>
        <Ind>a</Ind>
      </Expr>
      <Var>?X</Var>
    </Equal>
  </Query>
  <!-- 
  Result    
    Success
  
  Variable
    <Var>?X</Var>
  
  Values   
     <Data xsi:type="xs:integer">4</Data>
    
  -->

  <!-- Illustration of how reification differs from "passivation" via @per="copy".

          We may think of 
             * wrapping an expression with <Reify> or 
             * adding a semantic-variant attribute like @per="copy" 
         as "operators" on an undecorated nested expression:
         <Expr>
            <Fun>f</Fun>
            <Expr>
              <Fun>f</Fun>
              <Ind>a</Ind>
            </Expr>
          </Expr>
         
         Both of these "operators" prevent evaluation, but the effect of @per=copy
         is not inherited by nested expressions, while
         reification does passivate nested formulas and expressions to any depth.
         
    -->

  <Query>
    <!-- A query of KB1 for terms equal to the reification of a nested expression
         retrieves only the original reification, including the <Reify> wrapper.-->
    <Equal>
      <Reify>
        <Expr>
          <Fun>f</Fun>
          <Expr>
            <Fun>f</Fun>
            <Ind>a</Ind>
          </Expr>
        </Expr>
      </Reify>
      <Var>X</Var>
    </Equal>
  </Query>
  <!-- 
  Result
  Succeeds
  
  Variable
  <Var>X</Var>
  
  Values  
  <Reify>
    <Expr>
      <Fun>f</Fun>
      <Expr>
        <Fun>f</Fun>
        <Ind>a</Ind>
      </Expr>
    </Expr>
  </Reify>
  -->

  <Query>
    <!-- A query of KB1 for terms equal to a nested expression with the
      outer expression passivated by @per = "copy"
      retrieves an expression where the inner expression has been evaluated.-->
    <Equal>
      <Expr>
        <Fun per="copy">f</Fun>
        <Expr>
          <Fun per="value">f</Fun>
          <Ind>a</Ind>
        </Expr>
      </Expr>
      <Var>X</Var>
    </Equal>
  </Query>
  <!-- 
    Result
    Success
    
    Variable
    <Var>X</Var>
    
    Values     
    <Expr>
      <Fun per="copy">f</Fun>
      <Data xsi:type="xs:integer">4</Data>
    </Expr>
  -->

  <!-- <RetractAll/> -->

  <Assert node="#KB2">
    <!--
      This KB illustrates an "isTrue" predicate, which will "undo" reification.
    -->

    <Forall>
      <Var>X</Var>
      <Equivalent>
        <Atom>
          <Rel iri="#isTrue"/>
          <Reify>
            <Atom>
              <Rel>P</Rel>
              <Var>X</Var>
            </Atom>
          </Reify>
        </Atom>
        <Atom>
          <Rel>P</Rel>
          <Var>X</Var>
        </Atom>
      </Equivalent>
    </Forall>

    <!-- Assertion of a fact. -->
    <Atom>
      <Rel>P</Rel>
      <Ind>A</Ind>
    </Atom>
  </Assert>

  <Query>
    <!-- Query of KB2 for the reification of true formulas. -->
    <Atom>
      <Rel iri="isTrue"/>
      <Var>Z</Var>
    </Atom>
  </Query>
  <!-- 
  Result    
    Success
    
  Variable  
    <Var>Z</Var>
  
  Values
    <Reify>
      <Atom>
        <Rel>P</Rel>
        <Ind>A</Ind>
      </Atom>
    </Reify>
  -->

  <!-- 
  The "isTrue" predicate used above is inspired by the similar predicate in IKL, which undoes 'that'.
  However, there are some important differences between
  IKL's 'that' and RuleML's <Reify>
  1. 'that' applies only to formulas, not terms, while <Reify> applies to both
  2. 'that' is referentially transparent for all names, 
  while <Reify> has limited referential transparency - 
  it is only referentially transparent to <Var>. 
  
  For example, in IKL
  
  (= Bill William)
  entails
  (= (that (Happy Bill)) (that (Happy William)))
  
  while in RuleML
-->
  <Assert node="#KB3">
    <Equal>
      <Ind>Bill</Ind>
      <Ind>William</Ind>
    </Equal>
  </Assert>

  <Query>
    <!-- A query of KB3 shows that substitution of constants is not
         allowed inside reification. -->
    <Equal>
      <Reify>
        <Atom>
          <Rel>Happy</Rel>
          <Ind>Bill</Ind>
        </Atom>
      </Reify>
      <Reify>
        <Atom>
          <Rel>Happy</Rel>
          <Ind>William</Ind>
        </Atom>
      </Reify>
    </Equal>
  </Query>

  <!-- 
  Result
  Failure-->

  <!-- A Pathological Case: to avoid binding an active expression (with @per="value")
       to a variable, in this query the variable unifies with a passivated expression.-->
  <Query>
    <Equal>
      <Reify>
        <Expr>
          <Fun per="value">f</Fun>
          <Ind>a</Ind>
        </Expr>
      </Reify>
      <Reify>
        <Var>X</Var>
      </Reify>
    </Equal>
  </Query>

  <!-- 
  Result
  Success
  
  Variable
  <Var>X</Var>
  
  <Value>
  <Expr>
    <Fun per="copy">f</Fun>
    <Ind>a</Ind>
  </Expr>
  -->


</RuleML>

