orbital.logic.trs
Class Substitutions

java.lang.Object
  orbital.logic.trs.Substitutions

public class Substitutions
extends java.lang.Object

Provides term substitution, unification methods and the λ-operator. This class also forms the basis of Term Rewrite Systems (TRS).

You can easily run a (possibly even infinite) Term Rewrite System (TRS) with substitutions, like

 // instantiate a substitution performing elemental term rewrite rules
 Substitution σ = ...;
 // for example, use explicit σ = [x*e→x]
 σ = Substitutions.getInstance(Arrays.asList(new Object[] {
      Substitutions.createExactMatcher(Operations.times.apply(Values.symbol("x"), Values.symbol("e")), Functions.constant(Values.symbol("x")))
 }));
 // run the Term Rewrite System with argument as input, upon termination
 Object result = Functionals.fixedPoint(σ, argument);
 

However, you might prefer parsing expressions for some elements of the substitution list, like in

 // instantiate a parser for mathematical notation
 MathExpressionSyntax syntax = new MathExpressionSyntax();
 // for example, use parsed σ = [x*e→x]
 σ = Substitutions.getInstance(Arrays.asList(new Object[] {
      Substitutions.createExactMatcher(syntax.createMathExpression("x*e"), Functions.constant(Values.symbol("x")))
 }));
 // run the Term Rewrite System with argument as input, upon termination
 Object result = Functionals.fixedPoint(σ, argument);
 

Term rewriting systems are often used to define operational semantics.

Additionally, there are incredibly many applications of the λ-operator in various kinds of context.

Author:

André Platzer

See Also:

Facade Pattern, lambda

Field Summary

static Substitution	id The identical substitution id=[].
static BinaryFunction	lambda The λ-operator of λ-Calculus.

Method Summary

static Substitution	compose(Substitution sigma, Substitution tau) compose two substitutions σ ∘ τ.
static Substitution.Matcher	createExactMatcher(java.lang.Object pattern) Create a new exact matcher that does not perform substitution.
static Substitution.Matcher	createExactMatcher(java.lang.Object pattern, java.lang.Object substitute) Create a new exact matcher that performs substitution.
static Substitution.Matcher	createSingleSidedMatcher(java.lang.Object pattern) Create a new single sided matcher with unification that does not perform substitution.
static Substitution.Matcher	createSingleSidedMatcher(java.lang.Object pattern, java.lang.Object substitute) Create a new single sided matcher with unification that performs substitution, without conditions.
static Substitution.Matcher	createSingleSidedMatcher(java.lang.Object pattern, java.lang.Object substitute, Predicate condition) Create a new single sided matcher with unification that performs a substitution under a given condition.
static Substitution	getInstance(java.util.Collection replacements) Create a new substitution.
static Substitution	getInstance(java.util.Collection replacements, boolean typeSafe) Create a new substitution.
static boolean	isVariable(java.lang.Object x) Checks whether x is a variable.
static Function	lambda(java.lang.Object x, java.lang.Object f) Get the λ-abstraction of f with respect to x.
static Substitution	unify(java.util.Collection T) Unifies terms and returns "the" most general unifier mgU.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

id

public static final Substitution id

The identical substitution id=[].

This substitution has an empty list of replacements and thus performs nothing.

lambda

public static final BinaryFunction lambda

The λ-operator of λ-Calculus.

λ:σ×τ→(σ→τ); (λx.f) ↦ (x↦f)

Usually for σ=Variable, τ=Expression. Here λ is the formal parameter marker.

The λ-Calculus of Alonzo Church (1930) has the following inference rules called α-conversion, β-conversion, and η-conversion.

(α)	λv.t = λw.t[v→w]	if [v→w] is admissible, i.e. w∉FV(t)	"bound rename"
(β)	(λv.t) s = t[v→s]	if [v→s] is admissible	"apply"
(η)	λv.(t v) = t	if v∉FV(t)
(ext)	f(x)=g(x) implies f=g	if x∉FV(Ass∪{f,g})	"extensionality"

The η-conversion and extensionality are equivalent given the other axioms. A substitution t[v→s] is admissible if it does not introduce new bindings, i.e. no free variable of s would be bound by a λ-operator in t[v→s]. Typed λ-calculus satisfies strong normalization and Church-Rosser properties (with unique normal forms up to α-conversion).

Applying the λ-operator to a variable x and an expression f results in the λ-abstraction (λx.f) which is a unary function. This λ-abstraction could be circumscribed as the "function f with respect to x". λ is the inverse operator of function application.

The λ-operator is of course implemented as the substitution f[x→#0]. Note that this implementation does not strictly depend on x being an instance of Variable and f being an instance of Expression. Otherwise it will work fine just as well.

Implementation notes

If you experience troubles in the context of composite functions, then make sure which way of composition you have applied for f. Due to the mechanism of composition you may have to wrap, say a symbol x inside a constant function in order to get a function of f with respect to x as expected. So then you could try using

 Function h = Substitutions.lambda(Functions.constant(x), f);
 

instead.

Method Detail

getInstance

public static final Substitution getInstance(java.util.Collection replacements)

Create a new substitution.

See Also:

getInstance(Collection,boolean), "FacadeFactory"

getInstance

public static final Substitution getInstance(java.util.Collection replacements,
                                             boolean typeSafe)

Create a new substitution.

Note that you should not try to instantiate a "substitution" with multiple replacements specified for a single pattern. Those are not even endomorphisms anyway.

Parameters:

replacements - the set of elementary replacements, each specified by an implementation of Substitution.Matcher.

typeSafe - whether to instantiate a type-safe substitution, i.e. one for which [x:σ→t:τ] is only defined, when τ ≤ σ.

Returns:

σ = [replacements].

Throws:

TypeException - when typeSafe=true, but a type error occurs within the replacements.

See Also:

"FacadeFactory"

Preconditions:

replacements[i] instanceof Substitution.Matcher ∧ ∀i≠j replacements[i].pattern()≠replacements[j].pattern()

createExactMatcher

public static final Substitution.Matcher createExactMatcher(java.lang.Object pattern,
                                                            java.lang.Object substitute)

Create a new exact matcher that performs substitution.

This matcher performs exact matching with means of Object.equals(Object), only. Additionally it will directly replace with the specified substitute object.

Parameters:

pattern - The object against which to match with Object.equals(Object).

See Also:

"FacadeFactory"

createExactMatcher

public static final Substitution.Matcher createExactMatcher(java.lang.Object pattern)

Create a new exact matcher that does not perform substitution.

This matcher performs exact matching with means of Object.equals(Object), only.

Parameters:

pattern - The object against which to match with Object.equals(Object).

See Also:

"FacadeFactory"

createSingleSidedMatcher

public static final Substitution.Matcher createSingleSidedMatcher(java.lang.Object pattern,
                                                                  java.lang.Object substitute,
                                                                  Predicate condition)

Create a new single sided matcher with unification that performs a substitution under a given condition.

This matcher performs (single sided) matching with means of unify(Collection). (See there for a formal definition of single sided matchers). Additionally, if μ∈mgU({pattern, t}) is the unifier, it will use μ(substitute) as a replacement for the specified object t. However, only those matches μ that satisfy the specified condition predicate will be replaced.

Consider a rewrite rule

x₁+x₂ → x₂ /; x₁=0 which matches on occurrences of the form x₁+x₂ that will be replaced by the counterpart μ(x₂) of x₂ whenever condition(μ) holds, which is that the counterpart μ(x₁) of x₁ equals zero. Here, μ is the single side matcher substitution that will be passed to the condition predicate. For example, an occurrence of (6-3*2)+(5*b) matches to the pattern x₁+x₂ by μ={x₁→(6-3*2),x₂→(5*b)}. Since--after some evaluation--the condition predicate determines that the counterpart μ(x₁)=(6-3*2) turns out to be zero, a replacement to the substitute μ(x₂)=(5*b) will happen with a rewrite on the basis of the above conditional matcher.

☡ Beware of patterns for single sided matchers, that have variables in common with the terms it is applied on. This will most possibly lead to unexpected results. It is generally recommended to use uncommon variable names for these internal patterns, like _X1, _X2, _X3, ... or $X1, $X2, $X3, .... These uncommon variable names should not occur in regular terms then.

Parameters:

pattern - The object against which to (single side) match with unify(Collection).

substitute - The substitute substituting terms that matched, after transforming substitute with the unifier that performed the matching.

condition - The additional condition that has to hold for a match. Thus, this condition has to hold for occurrences that match (single sidedly) with pattern. The matcher returned will only match when condition.apply(μ) is true for the single sided matcher (resp. unifier) μ.

See Also:

"FacadeFactory"

createSingleSidedMatcher

public static final Substitution.Matcher createSingleSidedMatcher(java.lang.Object pattern,
                                                                  java.lang.Object substitute)

Create a new single sided matcher with unification that performs substitution, without conditions.

Parameters:

pattern - The object against which to (single side) match with unify(Collection).

substitute - The substitute substituting terms that matched, after transforming substitute with the unifier that performed the matching.

See Also:

createSingleSidedMatcher(Object, Object, Predicate), "FacadeFactory"

createSingleSidedMatcher

public static final Substitution.Matcher createSingleSidedMatcher(java.lang.Object pattern)

Create a new single sided matcher with unification that does not perform substitution.

Parameters:

pattern - The object against which to (single side) match with unify(Collection).

See Also:

createSingleSidedMatcher(Object, Object, Predicate), "FacadeFactory"

compose

public static final Substitution compose(Substitution sigma,
                                         Substitution tau)

compose two substitutions σ ∘ τ.

Get a performance optimized version of a composition of two substitutions.

Parameters:

sigma - the outer substitution σ.

tau - the inner substitution τ.

Returns:

σ ∘ τ = [x↦σ(t) ¦ (x↦t) ∈ τ] ∪ {(x↦t) ∈ σ ¦ ¬∃r (x↦r) ∈ τ}.

See Also:

Functionals.compose(Function, Function)

lambda

public static final Function lambda(java.lang.Object x,
                                    java.lang.Object f)

Get the λ-abstraction of f with respect to x.

This is only a shortcut for applying lambda(x,f) and solely for convenience.

Parameters:

x - the variable from whose exact name to abstract the term f. This means that the resulting λ-abstraction is a function in the variable x.

f - the term from which to build a λ-abstraction.

Returns:

the λ-abstraction λx.f

See Also:

lambda

Preconditions:

true (and usually x instanceof Variable, f instanceof Expression)

Postconditions:

RES.apply(a) = f[x->a]

unify

public static final Substitution unify(java.util.Collection T)

Unifies terms and returns "the" most general unifier mgU.

as set		prosa
U(T) :=	{σ ¦ 1 = |σ(T)|}	σ is a unifier of T⊆Term(Σ)
	σ(s)=σ(t)=t i.e. σ(s) is a sub term of t	σ is a single side matcher of s∈Term(Σ) on t∈Term(Σ)
mgU(T) :=	{μ ¦ ∀σ∈U(T) ∃σ’∈U(T) σ = σ’ ∘ μ}	μ is a most general unifier of T⊆Term(Σ). In fact, μ is a maximal element with respect to "σ|τ :⇔ ∃σ' τ = σ' ∘ σ"
UE(T) :=	{σ ¦ ∀i∈{1,..,n} σ(si) =E σ(ti)}	σ is an E-Unifier of Γ=⟨s1=t1,...s n=tn⟩

T unifiable (i.e. U(T)≠∅) ⇒ ∃μ∈mgU(T) μ is idempotent

μ,μ‘∈mgU(T) ⇒ ∃σ σ is a variable renaming ∧ μ = σ ∘ μ‘

Note that unification depends heavily on the identification of variables vs. constants.

Parameters:

T - a collection of terms to try to unify.

Returns:

mgU(T), the idempotent most-general unifier of T, or null if the terms in T are not unifiable.

Postconditions:

unifiable(T) ⇔ RES≠null ⇔ ∀t1,t2∈T RES.apply(t1).equals(RES.apply(t2))

isVariable

public static final boolean isVariable(java.lang.Object x)

Checks whether x is a variable.

See Also:

Convenience method, Variable.isVariable()

Postconditions:

RES = x instanceof Variable && ((Variable)x).isVariable()