Overview  Index  Help 

TERMS

All Known Implementing Modules:

TermsTermMatchUnifProofInfer


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.

           
Value summary

val alpha : ProofAst.ident -> ProofAst.ident
           gives a new fresh variable with the given identifier.

val alphaConvProc
    : (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.

val alphaEqual : ProofAst.formula * ProofAst.formula -> bool
           check the equality of a pair of formulas up to alpha-equivalence.

val fv_formulas : ProofAst.formula list -> ProofAst.ident list
           calculates the free variables of a formula list.

val fv_term : ProofAst.term -> ProofAst.ident list
           calculates the free variables of a term.

val substitute
    : ProofAst.ident -> ProofAst.term -> ProofAst.formula -> ProofAst.formula

           performs the substitution of a term into a formula.

val substituteAll
    : ProofAst.ident ->
        ProofAst.term ->
          (ProofAst.ident * ProofAst.formula) list ->
            (ProofAst.ident * ProofAst.formula) list

           performs a substitution into a named formula list.

val substituteAllList
    : (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.

val substituteList
    : (ProofAst.ident * ProofAst.term) list ->
        ProofAst.formula -> ProofAst.formula

           performs a list of substitutions into a formula.

 

       
Value detail

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.

 


Overview  Index  Help