[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification OUTREDUCE
enrich reduce , 
       termfuns , 
       nat-even
 with
comment: first try toplevel reduction (empty context). 
         Then try reduction of function, then of argument.;
   constants 
      I : term;
      SII : term;
   procedures 
      RED1  term : term_or_none; comment: either reduces term by on step or returns none.;
      TOPRED  term : term_or_none; comment: either reduces term by on step with empty context or returns none.;
      RED  term : term; comment: reduces term as long as possible;
   
   axioms 
      I-def :  ⊦ I = S _ K _ K;
      used for : s, ls;
       
      SII-def :  ⊦ SII = S _ I _ I;
      used for : s, ls;
       
declaration 
   RED1 (t; tn)
     { 
        TOPRED(t; tn) ; 
        if tn = none ∧ ap(t)
        then { 
                RED1(t .1; tn) ; 
                if tn ≠ none
                then tn := some(tn .t _ t .2)
                else if value(t .1)
                     then { 
                             RED1(t .2; tn) ; if tn ≠ none
                             then tn := some(t .1 _ tn .t)
                          }
             }
     };
   TOPRED (t; tn)
     { 
        if ap(t) ∧ ap(t .1) ∧ t .1 .1 = K ∧ value(t .1 .2) ∧ value(t .2)
        then tn := some(t .1 .2)
        else if ap(t) ∧ ap(t .1) ∧ ap(t .1 .1) ∧ t .1 .1 .1 = S
             then let v1 = t .1 .1 .2, v2 = t .1 .2, v3 = t .2
                  in if value(v1) ∧ value(v2) ∧ value(v3)
                     then tn := some(v1 _ v3 _ (v2 _ v3))
                     else tn := none
             else tn := none
     };
   RED (t; t0)
     { 
        let tn = none in { 
                            RED1(t; tn) ; if tn ≠ none
                            then RED(tn .t; t0)
                            else t0 := t
                         }
     };
end enrich