2.49. 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/tutorial/tut-1.49-0.flx[1 /1 ]
     1: #line 4628 "./lpsrc/flx_tutorial.pak"
     2: //Check axioms
     3: //Check reductions
     4: type int = "int";
     5: type string = "std::string";
     6: 
     7: typedef bool = 2;
     8: 
     9: fun add: int * int -> int = "$1+$2";
    10: fun mul: int * int -> int = "$1*$2";
    11: fun le: int * int -> bool = "$1<=$2";
    12: fun eq: int * int -> bool = "$1==$2";
    13: 
    14: header '#include <iostream>';
    15: header '#include <string>';
    16: proc print[t]: t = "std::cout<<$1;";
    17: proc endl: 1 = "std::cout<<std::endl;";
    18: 
    19: noinline fun f(x:int):int = { print "Cheat"; endl; return x; }
    20: 
    21: reduce idem(x:int): f ( f x ) => f x;
    22: 
    23: var x = f(f(f(f(1))));
    24: print x; endl;
    25: 
    26: axiom symmetry (x:int,y:int): x + y == y + x;
    27: axiom associativity (x:int, y:int, z:int): (x + y) + z == x + (y + z);
    28: reduce additive_unit(x:int): x + 0 => x;
    29: reduce multiplicative_unit(x:int): x * 0 => 0;
    30: reduce additive_unit(x:int): 0 + x => x;
    31: reduce multiplicative_unit(x:int): 0 * x=> 0;
    32: 
    33: //axiom wrong(x:int,y:int): x == y;
    34: fun hh(x:int)=>x;
    35: 
    36: reduce silly (x:int): hh x => x;
    37: 
    38: axiom_check (1,2,3);
    39: 
    40: var i:int=1;
    41: lab:>
    42:   axiom_check (i,2);
    43:   i=i+1;
    44:   if i <= 5  goto lab;
    45: 
    46: axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t):
    47:   sym(x,y) == sym(y,x)
    48: ;
    49: 
    50: axiom_check (add of (int * int), eq of (int * int), 1,2);
    51: 
    52: 
End felix section to tut/tutorial/tut-1.49-0.flx[1]
Start data section to tut/tutorial/tut-1.49-0.expect[1 /1 ]
     1: Cheat
     2: 1
End data section to tut/tutorial/tut-1.49-0.expect[1]