
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
java.lang.Object orbital.logic.trs.Substitutions
public class Substitutions
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.
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 

public static final Substitution id
This substitution has an empty list of replacements and thus performs nothing.
public static final BinaryFunction lambda
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" 
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.
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 

public static final Substitution getInstance(java.util.Collection replacements)
getInstance(Collection,boolean)
,
"FacadeFactory"public static final Substitution getInstance(java.util.Collection replacements, boolean typeSafe)
Note that you should not try to instantiate a "substitution" with multiple replacements specified for a single pattern. Those are not even endomorphisms anyway.
replacements
 the set of elementary replacements,
each specified by an implementation of Substitution.Matcher
.typeSafe
 whether to instantiate a typesafe substitution, i.e. one for which
[x:σ→t:τ]
is only defined, when τ ≤ σ.
TypeException
 when typeSafe=true
, but
a type error occurs within the replacements.Substitution.Matcher
∧ ∀i≠j replacements[i].pattern()≠replacements[j].pattern()public static final Substitution.Matcher createExactMatcher(java.lang.Object pattern, java.lang.Object substitute)
This matcher performs exact matching with means of Object.equals(Object)
, only.
Additionally it will directly replace with the specified substitute object.
pattern
 The object against which to match with Object.equals(Object)
.public static final Substitution.Matcher createExactMatcher(java.lang.Object pattern)
This matcher performs exact matching with means of Object.equals(Object)
, only.
pattern
 The object against which to match with Object.equals(Object)
.public static final Substitution.Matcher createSingleSidedMatcher(java.lang.Object pattern, java.lang.Object substitute, Predicate 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
condition
(μ) holds,
which is that the counterpart μ(x_{1}) of x_{1}
equals zero. Here, μ is the single side matcher substitution that
will be passed to the condition predicate.
For example, an occurrence of (63*2)+(5*b)
matches to the pattern
x_{1}+x_{2} by μ={x_{1}→(63*2)
,x_{2}→(5*b)
}.
Sinceafter some evaluationthe condition predicate determines that
the counterpart μ(x_{1})=(63*2)
turns out to be
zero, a replacement to the substitute μ(x_{2})=(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.
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) μ.public static final Substitution.Matcher createSingleSidedMatcher(java.lang.Object pattern, java.lang.Object substitute)
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.createSingleSidedMatcher(Object, Object, Predicate)
,
"FacadeFactory"public static final Substitution.Matcher createSingleSidedMatcher(java.lang.Object pattern)
pattern
 The object against which to (single side) match with unify(Collection)
.createSingleSidedMatcher(Object, Object, Predicate)
,
"FacadeFactory"public static final Substitution compose(Substitution sigma, Substitution tau)
Get a performance optimized version of a composition of two substitutions.
sigma
 the outer substitution σ.tau
 the inner substitution τ.
Functionals.compose(Function, Function)
public static final Function lambda(java.lang.Object x, java.lang.Object f)
This is only a shortcut for applying lambda
(x,f) and solely for convenience.
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.
lambda
public static final Substitution unify(java.util.Collection T)
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(Σ). 
U_{E}(T) := 
{σ ¦ ∀i∈{1,..,n} σ(s_{i}) =_{E} σ(t_{i})} 
σ is an EUnifier of Γ=⟨s_{1}=t_{1},...s_{ n}=t_{n}⟩ 
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.
T
 a collection of terms to try to unify.
null
if the terms in T are not unifiable.public static final boolean isVariable(java.lang.Object x)
Variable.isVariable()

Orbital library 1.3.0: 11 Apr 2009 

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 