1.48. Axioms and Reductions

Felix allows you to specify rewriting rules called reductions. For example:
  reduce idem(x:int): f ( f x ) => f x;
Specifies f is idempotent, and f(f(x)) should be reduced to just f(x). Reductions are performed after inlining, and applied repeatly to all expressions until code is fully reduced. The name of a reduction is not significiant, it is for documentation only. Of course, reductions can be polymorphic.

Axioms are statements of laws, for example

  axiom symmetry (x:int,y:int): x + y == y + x;
states that integer addition is symmetric. Axioms can be checked by providing test cases via calls to the pseudo function 'axiom_check'.
  var i:int; forall i in 1 upto 5 do axiom_check (i,2); done;
Axiom checks can be disable by the flxg compiler switch
  --no-axiom-checks
otherwise every axiom is matched against every test case, and each on the matches generates an assertion. An error is printed and the program aborted if any check fails.

Start felix section to tut/examples/tut_beg157a.flx[1 /1 ]
     1: #line 2546 "./lpsrc/flx_tutorial.pak"
     2: #import <flx.flxh>
     3: 
     4: noinline fun f(x:int):int = { print "Cheat"; endl; return x; }
     5: 
     6: reduce idem(x:int): f ( f x ) => f x;
     7: 
     8: var x = f(f(f(f(1))));
     9: print x; endl;
    10: 
    11: axiom symmetry (x:int,y:int): x + y == y + x;
    12: axiom associativity (x:int, y:int, z:int): (x + y) + z == x + (y + z);
    13: reduce additive_unit(x:int): x + 0 => x;
    14: reduce multiplicative_unit(x:int): x * 0 => 0;
    15: reduce additive_unit(x:int): 0 + x => x;
    16: reduce multiplicative_unit(x:int): 0 * x=> 0;
    17: 
    18: //axiom wrong(x:int,y:int): x == y;
    19: fun hh(x:int)=>x;
    20: 
    21: reduce silly (x:int): hh x => x;
    22: 
    23: axiom_check (1,2,3);
    24: 
    25: var i:int; forall i in 1 upto 5 do axiom_check (i,2); done;
    26: 
    27: axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t):
    28:   sym(x,y) == sym(y,x)
    29: ;
    30: 
    31: // this axiom is only right if 'add' is symmetric
    32: axiom_check (add of (int * int), eq of (int * int), 1,2);
    33: 
End felix section to tut/examples/tut_beg157a.flx[1]