Orbital library

orbital.logic.trs
Interface Substitution

All Superinterfaces:
Function, Functor

public interface Substitution
extends Function

Term substitution function.

A (uniform) substitution σ is a total endomorphism σ:Term(Σ)→Term(Σ) with

m

σ(f(t1,…,tn))

= σ(f)(σ(t1),…,σ(tn))

∀f(t1,…,tn)∈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 Substitution.Matcher), i.e. a mapping σ0:V→Term(Σ) with

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."
Let σ be a substitution.
variable renaming
σ is a variable renaming :⇔ σ:V→V is injective ⇔ σ(V)⊆V ∧ σ|supp(σ) is injective
idempotent
σ is idempotent :⇔ σ ∘ σ = σ ⇔ supp(σ)∩σ(supp(σ))=∅ ⇔ no variable xi occurs in a tj.
If a variable substitution has a left-inverse variable substitution, then it is only a variable renaming. For variable substitutions that have a right-inverse variable substitution this is true if their supports are disjoint.

We denote a substitution σ of supp(σ)={x1,…,xn} replacing xi with ti by

σ = [x1→t1,x2→t2,…,xn→tn] = [t1/x1,t2/x2,…,tn/xn]
σ(t) is called an instance of the term t.

Substitutions are for computer science what permutations (finite symmetric group) are for mathematics.

Author:
André Platzer
See Also:
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

getReplacements

java.util.Collection getReplacements()
Get the set of elementary replacements.

For a substitution σ = [x1→t1,x2→t2,…,xn→tn] the set of elementary replacements is {x1→t1,x2→t2,…,xn→tn}. Those elementary replacements are each specified by an implementation of Substitution.Matcher.

Note that the return-type is not fixed to sets, but would just as well allow lists as implementations although the order is not relevant for variable substitutions.

Returns:
the list of matchers used for replacement in this substitution.

apply

java.lang.Object apply(java.lang.Object term)
Apply this substitution σ to term.

A (uniform) substitution [x→t] replaces all occurrences of x with t. Whereas for substitutions with multiple replacement directions [x1→t1,x2→t2,… xn→tn], only the first applicable replacement will be applied on subterms.

Specified by:
apply in interface Function
Parameters:
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.
Returns:
σ(term)
Throws:
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.
Preconditions:
"the Composites 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

Copyright © 1996-2009 André Platzer
All Rights Reserved.