rewrite: apply bvar domainofapplication

• From: Andreas Strotmann <andreas.strotmann@ualberta.ca>
• Date: Sat, 06 Jun 2009 13:01:52 -0600
• To: David Carlisle <davidc@nag.co.uk>
• CC: www-math@w3.org
• Message-ID: <4A2ABD20.1060804@ualberta.ca>

This rewrite rule changes the arity of H, which is highly unlikely to be correct:

<apply> H 
   D 
  <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar> v1 </bvar>
    ...
    <bvar> vn </bvar>
     A1 
  </bind>
  ...
  <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar> v1 </bvar>
    ...
    <bvar> vn </bvar>
     Am 
  </bind>
</apply>

I suggest replacing this by something like the following, interpreting domainofapplication 
as a restriction on the operator:

<apply> 
  <apply> <csymbol>restrict</csymbol> H D</apply> 
  <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar> v1 </bvar>
    ...
    <bvar> vn </bvar>
     A1 
  </bind>
  ...
  <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar> v1 </bvar>
    ...
    <bvar> vn </bvar>
     Am 
  </bind>
</apply>

Received on Saturday, 6 June 2009 19:02:36 UTC