A convenient operator to make it easier to parse terms.

It is just a shortcut to call Fol.parset.

s : string

The input string.

Returns: term

The term corresponding to the input, if this is valid.

Example

 !!! "sqrt(1 - power(cos(x + y,2)))"

 Fn("sqrt",[Fn("-",[Fn("1",[]);
                    Fn("power",[Fn("cos",[Fn("+",[Var "x"; Var "y"]);
                                         Fn("2",[])])])])])

Example

 !!! "sqrt(1 - power(cos(x + y,2"

Parses a list of strings into a list of terms.

tms : string list

The input string list.

Returns: term list

The list of parsed terms.

Example

 !!!>["0";"1"]

Parses a list of string list into a list of term lists.

tms : string list list

The input list of string list.

Returns: term list list

The list of parsed term lists.

Example

 !!!>>[["0";"1"];["0"]]

Parses an atomic term.

vs : string list

inp : string list

Returns: term * string list

Recursive descent parser of terms built up from an atomic term parser by cascading instances of parse infix in order of precedence, following the conventions with '^' coming highest and '::' lowest.

It takes a list of string tokens `inp` and returns a pair consisting of the parsed term tree together with any unparsed input.

In order to check whether a name is within the scope of a quantifier, it takes an additional argument `vs` which is the set of bound variables in the current scope.

vs : string list

inp : string list

Returns: term * string list

Parses a string into a term.

s : string

The input string.

Returns: term

The term corresponding to the input, if this is valid.

Example

 parset "sqrt(1 - power(cos(x + y,2)))"

 Fn("sqrt",[Fn("-",[Fn("1",[]);
                    Fn("power",[Fn("cos",[Fn("+",[Var "x"; Var "y"]);
                                         Fn("2",[])])])])])

Example

 parset "sqrt(1 - power(cos(x + y,2"

A convenient operator to make it easier to parse formulas.

It is just a shortcut to call Fol.parse.

s : string

The input string.

Returns: formula<fol>

The fol formula corresponding to the input, if this is syntactically valid.

Example

 parse "x + y < z"

Example

 parse "x + y"

A convenient operator to make it easier to parse list of formulas.

xs : string list

Returns: formula<fol> list

The list of fol formulas corresponding to the input, if this is syntactically valid.

Example

 !!>["P(x)";"Q(x)"]

Parses string into a fol formula.

s : string

The input string.

Returns: formula<fol>

The fol formula corresponding to the input, if this is valid.

Example

 parse "x + y < z"

Example

 parse "x + y"

Parses atomic fol

vs : string list

inp : string list

Returns: formula<fol> * string list

A special recognizer for 'infix' atomic formulas like s < t.

vs : string list

inp : string list

Returns: formula<fol> * string list

Prints a function and its arguments.

tw : TextWriter

f : string

args : term list

Prints an infix operation.

tw : TextWriter

isleft : bool

oldprec : int

newprec : int

sym : string

p : term

q : term

Prints terms.

tw : TextWriter

prec : int

fm : term

Term printer with TextWriter.

tw : TextWriter

tm : term

Prints to the stdout the concrete syntax representation of a term.

t : term

The input term.

Example

 Fn("sqrt",[Fn("-",[Fn("1",[]);
                    Fn("power",[Fn("cos",[Fn("+",[Var "x"; Var "y"]);
                                         Fn("2",[])])])])])
 |> print_term

Returns the concrete syntax representation of a term.

Use the interactive option

 fsi.AddPrinter sprint_term

t : term

The input term.

Returns: string

The terms's concrete syntax representation.

Note

The opening and closing quotation symbols <<||>> used in the Handbook for terms have been here replaced with ````.

Example

 Fn("sqrt",[Fn("-",[Fn("1",[]);
                    Fn("power",[Fn("cos",[Fn("+",[Var "x"; Var "y"]);
                                         Fn("2",[])])])])])
 |> sprint_term

Returns a list of terms with the concrete syntax representation of terms.

tms : term list

Returns: string list

Note

This function is not part of che book code and is added here for convenience.

Returns a list of term lists with the concrete syntax representation of terms.

tms : term list list

Returns: string list list

Note

This function is not part of che book code and is added here for convenience.

Printer of atomic fol formulas with TextWriter.

tw : TextWriter

prec : 'a

arg2 : fol

Printer of fol formulas with TextWriter.

tw : TextWriter

Returns: formula<fol> -> unit

Printer of fol formulas to latex with TextWriter.

tw : TextWriter

Returns: formula<fol> -> unit

Printer of atomic fol

prec : 'a

arg : fol

Prints to the stdout the concrete syntax representation of a fol formula.

f : formula<fol>

The input formula.

Example

 Forall
 ("x",
  Forall
    ("y",
     Exists
       ("z",
        And
          (Atom (R ("<", [Var "x"; Var "z"])),
           Atom (R ("<", [Var "y"; Var "z"]))))))

Prints to the stdout the latex syntax of a fol formula.

f : formula<fol>

Returns the concrete syntax representation of an atom.

prec : 'a

arg : fol

Returns: string

Returns the concrete syntax representation of a fol formula.

Use the interactive option

 fsi.AddPrinter sprint_fol_formula

f : formula<fol>

The input formula.

Returns: string

The formula's concrete syntax representation.

Note

The opening and closing quotation symbols <<||>> used in the Handbook for terms have been here replaced with ``.

Example

 Forall
 ("x",
  Forall
    ("y",
     Exists
       ("z",
        And
          (Atom (R ("<", [Var "x"; Var "z"])),
           Atom (R ("<", [Var "y"; Var "z"]))))))
 |> sprint_fol_formula

Returns the latex syntax of a fol formula.

f : formula<fol>

Returns: string

Evaluates a fol formula fm in the interpretation (say \(M\)) specified by the triplet domain, func, pred and the variables valuation v.

domain : 'a list

The domain of the interpretation: the non-empty set \(D\) in which the value of each term lies.

func : string -> 'a list -> 'a

The mapping of each \(n\)-ary function symbol to a function \(f_M : D^n \rightarrow D\).

pred : string -> 'a list -> bool

The mapping of each \(n\)-ary predicate symbol to a boolean function \(P_M : D^n \rightarrow \{falso,vero\}\).

v : func<string, 'a>

The valuation of the variables: an fpf that maps each variable to an element of the domain.

fm : formula<fol>

The input formula.

Returns: bool

The truth-value of the formula in the given interpretation and valuation.

Example

 let fm = !! @"forall x. (x = 0) \/ (x = 1)" 
   
 holds bool_interp undefined fm    // evaluates to true
 holds (mod_interp 2) undefined fm // evaluates to true
 holds (mod_interp 3) undefined fm // evaluates to false

Returns the value of a term tm in the interpretation (say \(M\)) specified by the triplet domain, func, pred and valuation v.

domain : 'a

The domain of the interpretation: the non-empty set \(D\) in which the value of each term lies.

func : string -> 'b list -> 'b

The mapping of each \(n\)-ary function symbol to a function \(f_M : D^n \rightarrow D\).

pred : 'c

The mapping of each \(n\)-ary predicate symbol to a boolean function \(P_M : D^n \rightarrow \{falso,vero\}\).

v : func<string, 'b>

The valuation of the variables: an fpf that maps each variable to an element of the domain.

tm : term

The input term.

Returns: 'b

The element of the domain that corresponds to the term value in the given interpretation and valuation.

Example

 !!! "0" |> termval bool_interp undefined    // evaluates to false
 !!! "0" |> termval (mod_interp 3) undefined // evaluates to 0

An interpretation a la Boole.

Returns: bool list * (string -> bool list -> bool) * (string -> 'a list -> bool)

• Domain \(\{true, false\}\)
• Function symbols mapping: \(\text{0} \mapsto false, \text{1} \mapsto true, \text{+} \mapsto \lor, * \mapsto \land\)
• Predicate symbols mapping: \(\text{=} \mapsto =\)

An arithmetic modulo n interpretation.

n : int

The input modulo.

Returns: int list * (string -> int list -> int) * (string -> 'a list -> bool)

• Domain \(\{0,\ldots, n-1\}\)
• Function symbols mapping: \(\text{0} \mapsto 0, \text{1} \mapsto 1 \mod n, \text{+} \mapsto (x + y) \mod n, * \mapsto (x * y) \mod n\)
• Predicate symbols mapping: \(\text{=} \mapsto =\)

Example

 !!! "0" |> termval (mod_interp 3) undefined                 // evaluates to 0
 !!! "1" |> termval (mod_interp 3) undefined                 // evaluates to 1
 !!! "1 + 1" |> termval (mod_interp 3) undefined             // evaluates to 2
 !!! "1 + 1 + 1" |> termval (mod_interp 3) undefined         // evaluates to 0
 !!! "1 + 1 + 1 + 1" |> termval (mod_interp 3) undefined     // evaluates to 1
 !!! "1 + 1 + 1 + 1 + 1" |> termval (mod_interp 3) undefined // evaluates to 2

Returns the free variables in the fol formula fm.

fm : formula<fol>

The input formula.

Returns: string list

The list of the free variables in the formula fm

Example

 fv !!"forall x. x + f(y,z) > w"

Returns the free variables in the term tm.

tm : term

The input term.

Returns: string list

The list of free variables in the term tm

Example

 fvt !!!"x + f(y,z)"

Returns all the variables in the fol formula fm.

fm : formula<fol>

The input formula.

Returns: string list

The list of all the variables in the formula fm

Example

 var !!"forall x. x + f(y,z) > w"

Applies the substitution function subfn to fm.

Bound variables will be renamed if necessary to avoid capture.

subfn : func<string, term>

The fpf that contains the mapping for the variables to replace.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The formula obtained from fm by replacing its variables with the given mappings.

Example

 subst ("y" |=> Var "x") !!"forall x. x = y"

Example

 !!"forall x x'. x = y ==> x = x'"
 |> subst ("y" |=> Var "x")

Checks for variable captures in quantified formulas substitutions.

Checks whether there would be variable capture if the bound variable x is not renamed and, if so, creates the appropriate variants.

subfn : func<string, term>

The fpf that contains the mapping for the variables to replace.

quant : string -> formula<fol> -> formula<fol>

The quantification constructor to apply when reconstructing a quantified formula.

x : string

The variable to check.

p : formula<fol>

The input formula.

Returns: formula<fol>

The reconstructed quantified formula with appropriate variables variants if needed.

Example

 substq ("y" |=> Var "x") mk_forall "x" !!"x = y"

Applies the substitution function subfn to tm.

Replaces every variable in tm that matches an argument of sfn with its value.

subfn : func<string, term>

The fpf that contains the mapping for the variables to replace.

tm : term

The input term.

Returns: term

The term obtained from tm by replacing its variables with the given mappings.

Example

 !!!"x + f(y,z)" 
 |> tsubst (fpf ["x";"z"] [!!!"1";!!!"2"])

Creates a variant of the variable name x given a list of names (vars) to avoid.

Creates a 'variant' of a variable name by adding prime characters to it until it is distinct from every element of vars.

x : string

The input variable name.

vars : string list

The list of names to avoid.

Returns: string

The x itself it if is not contained in vars; otherwise, the string obtained from x adding prime characters to it until it is distinct from every element of vars.

Example

 variant "x" ["y"; "z"]  // evaluates to "x"
 variant "x" ["x"; "y"]  // evaluates to "x'"
 variant "x" ["x"; "x'"] // evaluates to "x''"

Universal closure of a formula.

Binds every free variable in the formula with a universal quantifier.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The universal closure of fm.

Example

 generalize !!"x + f(y,z) > w"

Checks if a string is a constant term.

Only numerals and the empty list constant nil are considered as constants.

s : string

The input string.

Returns: bool

true, if the input is a constant term, otherwise false.

Example

 is_const_name "nil" // evaluates to true
 is_const_name "123" // evaluates to true
 is_const_name "x"   // evaluates to false

Applies a function f to all the top terms in a fol formula fm, but otherwise leaves the structure unchanged.

It is similar to Formulas.onatoms but specific for fol formulas.

f : term -> term

The function to apply.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The result of applying f.

Example

 !! "P(x,f(z)) ==> Q(x)"
 |> onformula (function 
     | Var x -> Var (x + "_1") 
     | tm -> tm
 )