org.xmloperator.lambda.tree.reduction
Class TreeBetaUtils

java.lang.Object
  |
  +--org.xmloperator.lambda.tree.reduction.TreeBetaUtils

public abstract class TreeBetaUtils
extends java.lang.Object

Utilities about beta reduction.


Constructor Summary
TreeBetaUtils()
           
 
Method Summary
static Application leftermostOutermostRedex(Term rootTerm)
          Returns the leftermost-outermost redex of a Term or null if the Term has no redex.
static void main(java.lang.String[] args)
           
static Term reduce(Application redex)
          Reduces a redex.
static Term reduceDeeply(Term rootTerm, org.xmloperator.lambda.tree.reduction.ReductionListener reductionListener)
          Reduces a Term until a normal form is obtained.
static boolean test(java.io.PrintStream out, boolean isVerbose)
          Reduce some redexes and display the results.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

TreeBetaUtils

public TreeBetaUtils()
Method Detail

leftermostOutermostRedex

public static final Application leftermostOutermostRedex(Term rootTerm)
Returns the leftermost-outermost redex of a Term or null if the Term has no redex.

Pre-condition: the given Term is normalized about end-of-scopes.

Normalisation about EndOfScopes, i.e. scope extrusion, can be verified by using AlphaUtils.verifyScopeExtrusion(Term).

Parameters:
rootTerm - a Term.
Returns:
the leftermost-outermost redex of the given Term or null if it has no redex.
Throws:
java.lang.NullPointerException - if the given Term is broken.

reduce

public static final Term reduce(Application redex)
Reduces a redex. Returns the resulting Term. Returns the redex Application and the redex Abstraction to the factory.

Pre-condition: the redex is normalized about EndOfScopes.

Post-condition: the redex is normalized about EndOfScopes.

Normalisation about EndOfScopes, i.e scope extrusion, can be verified by using AlphaUtils.verifyScopeExtrusion(Term).

Parameters:
redex - a redex to reduce.
Returns:
the resulting Term. This is the body of the redex Abstraction.
Throws:
java.lang.IllegalArgumentException - if the given redex is not a redex.
java.lang.NullPointerException - if the given redex is broken.

reduceDeeply

public static final Term reduceDeeply(Term rootTerm,
                                      org.xmloperator.lambda.tree.reduction.ReductionListener reductionListener)
Reduces a Term until a normal form is obtained. The process may be aborted by a NotInNormalFormException thrown by ReductionListener.notifyStartReduction(org.xmloperator.lambda.tree.model.Application).

Parameters:
rootTerm - a Term to reduce.
reductionListener - a listener about beta-reduction process. May be null.
Returns:
the resulting Term.
Throws:
java.lang.NullPointerException - if the given root term is broken.
org.xmloperator.lambda.tree.exception.NotInNormalFormException - if the ReductionListener do so. The obtained Term is provided by the exception.

main

public static void main(java.lang.String[] args)

test

public static boolean test(java.io.PrintStream out,
                           boolean isVerbose)
Reduce some redexes and display the results.

Parameters:
out - the PrintStream to print results. May be null.
isVerbose - if true then all tests have to be displayed.
Returns:
true if all is Ok.