gapt/gapt/gapt.expr/gapt.expr.subst/Substitution

Substitution

gapt.expr.subst.Substitution

See theSubstitution companion object

class Substitution(map: Map[Var, Expr], typeMap: Map[TVar, Ty]) extends PreSubstitution

A substitution is a mapping from variables to lambda-expressions which differs from the identity on finitely many variables. Therefore:

each variable is mapped to only one lambda expression
the order of the variable-mappings is irrelevant
all variable-mappings are applied simultaneously to a term i.e. {x |-> y, y |-> a}x = y and not a.

As the lambda calculus contains variable binders, substitution can only be defined up to alpha-equivalence. When applying a substitution, bound variables are renamed if needed.

Attributes

Companion: object
Source: Substitution.scala
Graph
Supertypes: class PreSubstitution

class Object

trait Matchable

class Any
Known subtypes: class FOLSubstitution

Members list

Value members

Concrete methods

Applies this substitution to an object.

Type parameters

T: The type of x.
U: The type of x substituted.

Value parameters

ev: Testifies that applying a Substitution to an element of type T will result in an element of type U.
x: The object to be substituted.

Attributes

Source: Substitution.scala

Attributes

Definition Classes: PreSubstitution
Source: Substitution.scala

Compose two substitutions such that (a compose b)(x) == a(b(x)).

Attributes

Source: Substitution.scala

Attributes

Source: Substitution.scala

Attributes

Source: Substitution.scala

Attributes

Source: Substitution.scala

Inherited methods

Attributes

Inherited from:: PreSubstitution
Source: PreSubstitution.scala

Attributes

Inherited from:: PreSubstitution
Source: PreSubstitution.scala

Attributes

Inherited from:: PreSubstitution
Source: PreSubstitution.scala

Attributes

Inherited from:: PreSubstitution
Source: PreSubstitution.scala

Compares the receiver object (this) with the argument object (that) for equivalence.

Any implementation of this method should be an equivalence relation:

It is reflexive: for any instance x of type Any, x.equals(x) should return true.
It is symmetric: for any instances x and y of type Any, x.equals(y) should return true if and only if y.equals(x) returns true.
It is transitive: for any instances x, y, and z of type Any if x.equals(y) returns true and y.equals(z) returns true, then x.equals(z) should return true.

If you override this method, you should verify that your implementation remains an equivalence relation. Additionally, when overriding this method it is usually necessary to override hashCode to ensure that objects which are "equal" (o1.equals(o2) returns true) hash to the same scala.Int. (o1.hashCode.equals(o2.hashCode)).

Value parameters

that: the object to compare against this object for equality.

Attributes

Returns: true if the receiver object is equivalent to the argument; false otherwise.
Definition Classes: PreSubstitution -> Any
Inherited from:: PreSubstitution
Source: PreSubstitution.scala

Calculate a hash code value for the object.

The default hashing algorithm is platform dependent.

Note that it is allowed for two objects to have identical hash codes (o1.hashCode.equals(o2.hashCode)) yet not be equal (o1.equals(o2) returns false). A degenerate implementation could always return 0. However, it is required that if two objects are equal (o1.equals(o2) returns true) that they have identical hash codes (o1.hashCode.equals(o2.hashCode)). Therefore, when overriding this method, be sure to verify that the behavior is consistent with the equals method.