Unif Module
Unification for first order terms.
Functions and values
| Function or value | Description | ||||
|
Returns an MGU for a list of term-term pairs
Example
[("x", ``0``); ("y", ``0``)].
Example
System.Exception: cyclic.
Example
System.Exception: cyclic.
|
||||
Full Usage:
istriv env x t
Parameters:
func<string, term>
-
The environment of mappings (represented as a finite partial function) from variables to terms in which to check the new assignment.
x : string
-
The variable to be assigned.
t : term
-
The term assigned to the variable.
Returns: bool
true, if the assignment is trivial (t = x); otherwise, if
there are no cycle, false.
|
Checks the new assignment
ExampleTrivial assignment true.
ExampleAcyclic nontrivial assignment false.
ExampleCyclic nontrivial assignment System.Exception: cyclic.
|
||||
Reduces an input unifier
Removes useless mappings from the input variable-term
mappings Note
The function never fails. However, it would cause a StackOverflow
crash if called on a cyclic ExampleThe following reduces \(x \mapsto y, x \mapsto 0\) to \(x \mapsto 0\). [("x", ``0``)].
ExampleThe following returns the input unchanged \(x \mapsto 1, y \mapsto 0\) since the input is already an MGU. [("x", ``1``); ("y", ``0``)].
ExampleThe following would cause a StackOverflow crash. |
|||||
Full Usage:
unify env eqs
Parameters:
func<string, term>
-
An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure.
eqs : (term * term) list
-
The list of term-term pairs to be unified.
Returns: func<string, term>
A variable-term mappings that unify eqs, if the unification is
possible and there are no cycles.
|
Returns a unifier for a list of term-term pairs
It applies some transformations to
ExampleNo previous assignments [("x", ``0``)].
ExampleAugmented assignment [("x", ``y``); ("y", ``0``)].
ExampleDirect cycle (\(y \mapsto f(y)\)) System.Exception: cyclic.
ExampleDerived cycle (\(x \mapsto y, y \mapsto f(x)\)) System.Exception: cyclic.
ExampleImpossible unification System.Exception: impossible unification.
|
||||
|
Finds and apply an MGU to a list of term-term pairs
Finds an MGU for a list of term-term pairs
Example
[(``f(f(z),g(y))``, ``f(f(z),g(y))``)].
Example
System.Exception: cyclic.
Example
System.Exception: impossible unification.
|