
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
public interface Substitution
Term substitution function.
A (uniform) substitution σ is a total endomorphism σ:Term(Σ)→Term(Σ) with 

m 
σ(f(t_{1},…,t_{n})) 
= σ(f)(σ(t_{1}),…,σ(t_{n})) 
∀f(t_{1},…,t_{n})∈Term(Σ) 
fin 
σ_{V} 
= id p.t. 
(⇔ supp(σ) := {x∈V ¦ σ(x)≠x} is finite) 
Note: Substitutions are usually restricted to "proper" variable substitutions that only substitute variables, i.e. σ(f)=f for functions and predicates. Often, variable substitutions are even restricted to admissible variable substitutions that only substitute free variables, such that it does not lead to collisions. Otherwise the application of a variable substitution would possibly introduce new (illegal) bindings inside the scope of a quantifier. 

A basic substitution (also see 

fin 
σ_{0} 
= id p.t. 
(⇔ supp(σ) := {x∈V ¦ σ(x)≠x} is finite) 
can be extended uniquely (UP) to a variable substitution σ:Term(Σ)→Term(Σ) such that σ_{V} = σ_{0}. 
"Substitutions are the homomorphic continuation of variable replacements."
We denote a substitution σ of supp(σ)={x_{1},…,x_{n}} replacing x_{i} with t_{i} by
Substitutions are for computer science what permutations (finite symmetric group) are for mathematics.
Substitutions
,
Substitutions.getInstance(Collection)
Nested Class Summary  

static interface 
Substitution.Matcher
Interface for matching and replacing elementary terms within a substitution. 
Nested classes/interfaces inherited from interface orbital.logic.functor.Function 

Function.Composite 
Nested classes/interfaces inherited from interface orbital.logic.functor.Functor 

Functor.Specification 
Field Summary 

Fields inherited from interface orbital.logic.functor.Function 

callTypeDeclaration 
Method Summary  

java.lang.Object 
apply(java.lang.Object term)
Apply this substitution σ to term. 
java.util.Collection 
getReplacements()
Get the set of elementary replacements. 
Methods inherited from interface orbital.logic.functor.Functor 

equals, hashCode, toString 
Method Detail 

java.util.Collection getReplacements()
For a substitution σ = [x_{1}→t_{1},x_{2}→t_{2},…,x_{n}→t_{n}]
the set of elementary replacements is
{x_{1}→t_{1},x_{2}→t_{2},…,x_{n}→t_{n}}.
Those elementary replacements are each specified by an
implementation of Substitution.Matcher
.
Note that the returntype is not fixed to sets, but would just as well allow lists as implementations although the order is not relevant for variable substitutions.
java.lang.Object apply(java.lang.Object term)
A (uniform) substitution [x→t] replaces all occurrences of x with t. Whereas for substitutions with multiple replacement directions [x_{1}→t_{1},x_{2}→t_{2},… x_{n}→t_{n}], only the first applicable replacement will be applied on subterms.
apply
in interface Function
term
 the term object that will be decomposed according to
Composite
for applying the substitution, with
variables identified via Variable.isVariable()
.
Substitutions automatically map
themselves over Collection
and arrays.
java.lang.ArrayStoreException
 if this method tried to store a part of the result in an array,
but the substitution list produced a replacement of an illegal type.
java.lang.ClassCastException
 if the substitution list produced a replacement of an illegal type.Composite
s occuring in term support Composite.construct(Object,Object)
in order to allow being substituted by an object of equal class"

Orbital library 1.3.0: 11 Apr 2009 

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