Substitution

sealed class Substitution: Map<Var, Term>, Any

An interface representing a mapping between Variables and their Term substitutions

Fields

Name Description
open isSuccess: Boolean

Whether this Substitution is a successful one (is a Unifier)

open isFailed: Boolean

Whether this Substitution is a failed one

Methods

applyTo

fun applyTo(term: Term): Term

Applies the Substitution to the given Term

Parameters

Name Description
term: Term

ReturnValue

Name Description
Term

getOriginal

abstract fun getOriginal(variable: Var): Var?

Retrieves the original variable name of the provided variable, if any, or null otherwise

Consider for instance the substitution { X -> Y, Y -> Z }, then the invocation of getOriginal(Z) should retrieve X

Parameters

Name Description
variable: Var

ReturnValue

Name Description
Var?

plus

operator fun plus(other: Substitution): Substitution

Creates a new substitution that's the composition of this and other

However additional checks are performed:

Parameters

Name Description
other: Substitution

ReturnValue

Name Description
Substitution

minus

open operator fun minus(keys: Iterable<Var>): Substitution

Returns a new substitution containing all entries of the original substitution except those entries which variable keys are contained in the given keys iterable.

Parameters

Name Description
keys: Iterable<Var>

ReturnValue

Name Description
Substitution

minus

open operator fun minus(other: Substitution): Substitution

Returns a new substitution containing all entries of the original substitution except those entries which variable keys are contained in the given other substitution.

Parameters

Name Description
other: Substitution

ReturnValue

Name Description
Substitution

filter

open fun filter(predicate: (Entry<Var, Term>)->Boolean): Substitution

Returns a new substitution containing all key-value pairs matching the given predicate.

The returned map preserves the entry iteration order of the original map.

Parameters

Name Description
predicate: (Entry<Var, Term>)->Boolean

ReturnValue

Name Description
Substitution

filter

open fun filter(variables: Collection<Var>): Substitution

Returns a new substitution containing all key-value pairs whose key is in variables.

The returned map preserves the entry iteration order of the original map.

Parameters

Name Description
variables: Collection<Var>

ReturnValue

Name Description
Substitution

filter

open fun filter(predicate: (Var, Term)->Boolean): Substitution

Returns a new substitution containing all key-value pairs matching the given predicate.

The returned map preserves the entry iteration order of the original map.

Parameters

Name Description
predicate: (Var, Term)->Boolean

ReturnValue

Name Description
Substitution

Extensions

toEquations

fun Substitution.toEquations(): List<Equation<Var, Term>>

Transforms a Substitution into the list of corresponding Equations

Receiver

Name Description
Substitution

ReturnValue

Name Description
List<Equation<Var, Term>>

CompanionObject

Substitution

sealed class Substitution: Map<Var, Term>, Any

An interface representing a mapping between Variables and their Term substitutions

Methods

failed

fun failed(): Fail

Returns failed substitution instance

ReturnValue

Name Description
Fail

empty

fun empty(): Unifier

Returns empty successful substitution (aka Unifier) instance

ReturnValue

Name Description
Unifier

asUnifier

fun Map<Var, Term>.asUnifier(): Unifier

Conversion from a raw Map to Successful Substitution (aka Unifier) type

Receiver

Name Description
Map<Var, Term>

ReturnValue

Name Description
Unifier

of

fun of(variable: Var, withTerm: Term): Unifier

Creates a Substitution of given Variable with given Term

Parameters

Name Description
variable: Var
withTerm: Term

ReturnValue

Name Description
Unifier

of

fun of(variable: String, withTerm: Term): Unifier

Creates a Substitution from the new Variable, with given name, to given Term

Parameters

Name Description
variable: String
withTerm: Term

ReturnValue

Name Description
Unifier

of

fun of(substitutionPair: Pair<Var, Term>, vararg substitutionPairs: Pair<Var, Term>): Substitution

Crates a Substitution from given substitution pairs; if any contradiction is found, the result will be Substitution.Fail

Parameters

Name Description
substitutionPair: Pair<Var, Term>
vararg substitutionPairs: Pair<Var, Term>

ReturnValue

Name Description
Substitution

of

fun of(substitutionPairs: Iterable<Pair<Var, Term>>): Substitution

Crates a Substitution from given substitution pairs; if any contradiction is found, the result will be Substitution.Fail

Parameters

Name Description
substitutionPairs: Iterable<Pair<Var, Term>>

ReturnValue

Name Description
Substitution

of

fun of(substitution: Substitution, vararg substitutions: Substitution): Substitution

Creates a new Substitution composing given substitutions in order; if any failure or contradiction is found, the result will be Substitution.Fail

Parameters

Name Description
substitution: Substitution
vararg substitutions: Substitution

ReturnValue

Name Description
Substitution