Substitution

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

General type for logic substitutions (i.e. variables assignments). There are two sorts of substitutions:

Substitution.Unifier, which represent one possible assignment for a possibly empty set of Vars
Substitution.Fail, which represent the lack of possible assignments for any set of Vars

Fields

Name	Description
`abstract isSuccess: Boolean`	Whether this Substitution is a successful one (i.e., a Unifier)
`abstract isFailed: Boolean`	Whether this Substitution is a failed one

Methods

asUnifier

open fun asUnifier(): Unifier?

Casts the current Substitution to Unifier, if possible, or returns null otherwise

ReturnValue

Name	Description
`Unifier?`	the current Substitution, casted to Unifier, or `null`, if the current term is not an instance of Unifier

castToUnifier

open fun castToUnifier(): Unifier

Casts the current Substitution to Unifier, if possible

ReturnValue

Name	Description
`Unifier`	the current Substitution, casted to Unifier

asFail

open fun asFail(): Fail?

Casts the current Substitution to Fail, if possible, or returns null otherwise

ReturnValue

Name	Description
`Fail?`	the current Substitution, casted to Fail, or `null`, if the current term is not an instance of Fail

castToFail

open fun castToFail(): Fail

Casts the current Substitution to Fail, if possible

ReturnValue

Name	Description
`Fail`	the current Substitution, casted to Fail

applyTo

abstract fun applyTo(term: Term): Term?

Applies this Substitution to the given Term, returning null if it is Substitution.Fail

Parameters

Name	Description
`term: Term`

ReturnValue

Name	Description
`Term?`

whenIs

abstract fun <T> whenIs(unifier: (Unifier)->T, fail: (Fail)->T, otherwise: (Substitution)->T): T

Parameters

Name	Description
`unifier: (Unifier)->T`
`fail: (Fail)->T`
`otherwise: (Substitution)->T`

ReturnValue

Name	Description
`T`

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?`

getByName

open fun getByName(name: String): Term?

Parameters

Name	Description
`name: String`

ReturnValue

Name	Description
`Term?`

plus

abstract operator fun plus(other: Substitution): Substitution

Creates a new Substitution that is the composition (a.k.a. union) of this and other. The composition is not guaranteed to be a Substitution.Unifier, even if both arguments are. In fact, the composition algorithm performs the following checks:

If one of arguments is of type Substitution.Fail, the result is of type Substitution.Fail
If the set of assignments attained by composing the two substitutions is contradictory -- i.e., if the same Var is assigned to different Terms --, the result is of type Substitution.Fail
Otherwise, the result is an instance of Substitution.Unifier

Regardless of its type, the resulting Substitution will contain the tags of both input Substitutions.

Parameters

Name	Description
`other: Substitution`

ReturnValue

Name	Description
`Substitution`

plus

abstract fun plus(other: Substitution, tagsMerger: TagsOperator): Substitution

If one of arguments is of type Substitution.Fail, the result is of type Substitution.Fail
If the set of assignments attained by composing the two substitutions is contradictory -- i.e., if the same Var is assigned to different Terms --, the result is of type Substitution.Fail
Otherwise, the result is an instance of Substitution.Unifier

Regardless of its type, the resulting Substitution will contain the tags attained by merging the input Substitutions' tags via tagsMerger.

Parameters

Name	Description
`other: Substitution`
`tagsMerger: TagsOperator`

ReturnValue

Name	Description
`Substitution`

minus

abstract 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.

Regardless of its type, the resulting Substitution will contain the same tags of the original one

Parameters

Name	Description
`keys: Iterable<Var>`

ReturnValue

Name	Description
`Substitution`

minus

abstract operator fun minus(variable: Var): Substitution

Parameters

Name	Description
`variable: Var`

ReturnValue

Name	Description
`Substitution`

minus

abstract fun minus(variable: Var, vararg otherVariables: Var): Substitution

Parameters

Name	Description
`variable: Var`
`vararg otherVariables: Var`

ReturnValue

Name	Description
`Substitution`

minus

abstract 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.

Regardless of its type, the resulting Substitution will contain the same tags of the original one

Parameters

Name	Description
`other: Substitution`

ReturnValue

Name	Description
`Substitution`

filter

abstract 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.

Regardless of its type, the resulting Substitution will contain the same tags of the original one

Parameters

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

ReturnValue

Name	Description
`Substitution`

filter

abstract 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.

Regardless of its type, the resulting Substitution will contain the same tags of the original one

Parameters

Name	Description
`variables: Collection<Var>`

ReturnValue

Name	Description
`Substitution`

filter

abstract 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>

Transforms a Substitution into the list of corresponding Equations

Receiver

Name	Description
`Substitution`

ReturnValue

Name	Description
`List<Equation>`

CompanionObject

Substitution

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

General type for logic substitutions (i.e. variables assignments). There are two sorts of substitutions:

Substitution.Unifier, which represent one possible assignment for a possibly empty set of Vars
Substitution.Fail, which represent the lack of possible assignments for any set of Vars

Methods

failed

fun failed(): Fail

Returns a failed substitution, i.e. an instance of type Substitution.Fail

ReturnValue

Name	Description
`Fail`

empty

fun empty(): Unifier

Returns an empty unifier, i.e. an instance of type Substitution.Fail

ReturnValue

Name	Description
`Unifier`

of

fun of(map: Map<Var, Term>): Unifier

Creates a Unifier of given a map assigning Vars to Terms

Parameters

Name	Description
`map: Map<Var, Term>`

ReturnValue

Name	Description
`Unifier`

of

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

Creates a singleton Unifier containing a single Var-Term assignment

Parameters

Name	Description
`variable: Var`
`term: Term`

ReturnValue

Name	Description
`Unifier`

of

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

Creates a singleton Unifier containing a single Var-Term assignment. The variable is created on the fly by name, via Var.of

Parameters

Name	Description
`variable: String`
`term: Term`

ReturnValue

Name	Description
`Unifier`

of

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

Crates a Substitution from the given Var-Terms. If any contradiction is found, an instance of Substitution.Fail is returned

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 the given Iterable of Var-Terms. If any contradiction is found, an instance of Substitution.Fail is returned

Parameters

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

ReturnValue

Name	Description
`Substitution`

of

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

Crates a Substitution from the given Sequence of Var-Terms. If any contradiction is found, an instance of Substitution.Fail is returned

Parameters

Name	Description
`substitutionPairs: Sequence><Pair<Var, Term>>`

ReturnValue

Name	Description
`Substitution`

of

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

Composes the provided Substitutions by merging them. 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`

unifier

fun unifier(map: Map<Var, Term>): Unifier

Creates a Unifier of given a map assigning Vars to Terms

Parameters

Name	Description
`map: Map<Var, Term>`

ReturnValue

Name	Description
`Unifier`

unifier

fun unifier(variable: Var, term: Term): Unifier

Creates a Unifier of given a map assigning Vars to Terms

Parameters

Name	Description
`variable: Var`
`term: Term`

ReturnValue

Name	Description
`Unifier`

unifier

fun unifier(variable: String, term: Term): Unifier

Creates a singleton Unifier containing a single Var-Term assignment. The variable is created on the fly by name, via Var.of

Parameters

Name	Description
`variable: String`
`term: Term`

ReturnValue

Name	Description
`Unifier`

unifier

fun unifier(substitutionPair: Pair<Var, Term>, vararg substitutionPairs: Pair<Var, Term>): Unifier

Crates a Substitution from the given Var-Terms. If any contradiction is found, a SubstitutionException is thrown

Parameters

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

ReturnValue

Name	Description
`Unifier`

unifier

fun unifier(map: Iterable<Pair<Var, Term>>): Unifier

Crates a Unifier from the given Iterable of Var-Terms. If any contradiction is found, a SubstitutionException is thrown

Parameters

Name	Description
`map: Iterable<Pair<Var, Term>>`

ReturnValue

Name	Description
`Unifier`

unifier

fun unifier(map: Sequence><Pair<Var, Term>>): Unifier

Crates a Unifier from the given Sequence of Var-Terms. If any contradiction is found, a SubstitutionException is thrown

Parameters

Name	Description
`map: Sequence><Pair<Var, Term>>`

ReturnValue

Name	Description
`Unifier`