TERMS
- All Known Implementing Modules:
-
Terms, TermMatchUnif, ProofInfer
-
The First-Order LoopW Type Inference formula/term substitution and alpha-equivalence.
Provides functions in order to calculate free variables, perform term substitution
into formulas/terms, and identify formulas up to alpha-equivalence.
-
alpha
fun alpha i : ProofAst.ident -> ProofAst.ident
-
gives a new fresh variable with the given identifier.
-
- Parameters:
-
-
i
-
the identifier.
- Returns:
-
a fresh identifier.
fv_term
fun fv_term t : ProofAst.term -> ProofAst.ident list
-
calculates the free variables of a term.
-
- Parameters:
-
-
t
-
the term.
- Returns:
-
the list of free identifiers.
fv_formulas
fun fv_formulas fl : ProofAst.formula list -> ProofAst.ident list
-
calculates the free variables of a formula list.
-
- Parameters:
-
-
fl
-
the formula list.
- Returns:
-
the list of free identifiers.
substitute
fun substitute x t f
: ProofAst.ident -> ProofAst.term -> ProofAst.formula -> ProofAst.formula
-
performs the substitution of a term into a formula.
-
- Parameters:
-
-
x
-
the identifier to be substituted.
-
t
-
the term to substitute to x.
-
f
-
the formula in which to perform the substitution.
- Returns:
-
the new formula f[t/x].
substituteList
fun substituteList xtlist f
: (ProofAst.ident * ProofAst.term) list ->
ProofAst.formula -> ProofAst.formula
-
performs a list of substitutions into a formula.
-
- Parameters:
-
-
xtlist
-
the list of substitutions to perform.
-
f
-
the formula in which to perform the substitution.
- Returns:
-
the new formula f[t1/x1, ..., tn/xn].
substituteAll
fun substituteAll x t yflist
: ProofAst.ident ->
ProofAst.term ->
(ProofAst.ident * ProofAst.formula) list ->
(ProofAst.ident * ProofAst.formula) list
-
performs a substitution into a named formula list.
-
- Parameters:
-
-
x
-
the identifier to be substituted.
-
t
-
the term to substitute to x.
-
yflist
-
the named formula list in which to perform the substitution.
- Returns:
-
the new formula [y,f][t/x].
substituteAllList
fun substituteAllList xtlist yflist
: (ProofAst.ident * ProofAst.term) list ->
(ProofAst.ident * ProofAst.formula) list ->
(ProofAst.ident * ProofAst.formula) list
-
performs a list of substitutions into a named formula list.
-
- Parameters:
-
-
xtlist
-
the list of substitutions to perform.
-
yflist
-
the named formula list in which to perform the substitution.
- Returns:
-
the new formula [y,f][t1/x1, ..., tn/xn].
alphaConvProc
fun alphaConvProc (f1, f2)
: (ProofAst.ident list *
ProofAst.formula list *
ProofAst.ident list *
ProofAst.formula list) *
(ProofAst.ident list *
ProofAst.formula list *
ProofAst.ident list *
ProofAst.formula list) ->
(ProofAst.ident list *
ProofAst.formula list *
ProofAst.ident list *
ProofAst.formula list) *
(ProofAst.ident list *
ProofAst.formula list *
ProofAst.ident list *
ProofAst.formula list)
-
converts the proc types in order to have the same bound variables.
-
- Parameters:
-
-
f1
-
the first formula proc({i} sigma; out {j} tau).
-
f2
-
the second formula proc({i'} sigma'; out {j'} tau').
- Returns:
-
(f1', f2') where f1 = proc({i''} sigma[i''/i]; out {j''} tau[j''/j]),
and f1 = proc({i''} sigma'[i''/i']; out {j''} tau'[j''/j']).
alphaEqual
fun alphaEqual (f1, f2) : ProofAst.formula * ProofAst.formula -> bool
-
check the equality of a pair of formulas up to alpha-equivalence.
-
- Parameters:
-
-
f1
-
the first formula to compare.
-
f2
-
the second formula to compare.
- Returns:
-
true if and only if f1 = f2 up to alpha-equivalence.