Formulas (Calculemus)

Formulas Module

Namespace: Calculemus
Assembly: Calculemus.dll

Polymorphic type of formulas with parser and printer.

Parsing
Prettyprinting
Destructors
Constructors
Syntax operations

Types

Type	Description
formula<'a>	Abstract syntax tree of polymorphic type of formulas.

Parsing

Functions and values

Function or value	Description
`parse_atomic_formula (ifn, afn) vs inp` Full Usage: `parse_atomic_formula (ifn, afn) vs inp` Parameters: ifn : `string list -> string list -> formula<'a> * string list` - A restricted parser for infix atoms. afn : `string list -> string list -> formula<'a> * string list` - A general parser for arbitrary atoms. vs : `string list` - The set of bound variables in the current scope. inp : `string list` - The list of string tokens Returns: `formula<'a> * string list` A pair consisting of the parsed formula tree together with any unparsed input.	Parses atomic formulas. It attempts to parse an atomic formula as a term followed by an infix predicate symbol and only if that fails proceed to considering other kinds of formulas. ifn : `string list -> string list -> formula<'a> * string list` A restricted parser for infix atoms. afn : `string list -> string list -> formula<'a> * string list` A general parser for arbitrary atoms. vs : `string list` The set of bound variables in the current scope. inp : `string list` The list of string tokens Returns: `formula<'a> * string list` A pair consisting of the parsed formula tree together with any unparsed input.
`parse_formula (ifn, afn) vs inp` Full Usage: `parse_formula (ifn, afn) vs inp` Parameters: ifn : `string list -> string list -> formula<'a> * string list` - A restricted parser for infix atoms. afn : `string list -> string list -> formula<'a> * string list` - A general parser for arbitrary atoms. vs : `string list` - The set of bound variables in the current scope. inp : `string list` - The list of string tokens Returns: `formula<'a> * string list` A pair consisting of the parsed formula tree together with any unparsed input.	Recursive descent parser of polymorphic formulas built up from an atomic formula 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 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. ifn : `string list -> string list -> formula<'a> * string list` A restricted parser for infix atoms. afn : `string list -> string list -> formula<'a> * string list` A general parser for arbitrary atoms. vs : `string list` The set of bound variables in the current scope. inp : `string list` The list of string tokens Returns: `formula<'a> * string list` A pair consisting of the parsed formula tree together with any unparsed input.
`parse_quant (ifn, afn) vs qcon x inp` Full Usage: `parse_quant (ifn, afn) vs qcon x inp` Parameters: ifn : `string list -> string list -> formula<'a> * string list` - A restricted parser for infix atoms. afn : `string list -> string list -> formula<'a> * string list` - A general parser for arbitrary atoms. vs : `string list` - The set of bound variables in the current scope. qcon : `string * formula<'a> -> formula<'a>` x : `string` inp : `string list` - The list of string tokens Returns: `formula<'a> * string list` A pair consisting of the parsed formula tree together with any unparsed input.	Parses quantified formulas. ifn : `string list -> string list -> formula<'a> * string list` A restricted parser for infix atoms. afn : `string list -> string list -> formula<'a> * string list` A general parser for arbitrary atoms. vs : `string list` The set of bound variables in the current scope. qcon : `string * formula<'a> -> formula<'a>` x : `string` inp : `string list` The list of string tokens Returns: `formula<'a> * string list` A pair consisting of the parsed formula tree together with any unparsed input.

Prettyprinting

Functions and values

Function or value	Description
`fbracket tw p n f x y` Full Usage: `fbracket tw p n f x y` Parameters: tw : `TextWriter` p : `bool` n : `'a` f : `'b -> 'c -> unit` x : `'b` y : `'c`	Modifies a basic printer to have a kind of boxing 'wrapped' around it. tw : `TextWriter` p : `bool` n : `'a` f : `'b -> 'c -> unit` x : `'b` y : `'c`
`fprint_formula tw pfn` Full Usage: `fprint_formula tw pfn` Parameters: tw : `TextWriter` pfn : `int -> 'a -> unit` Returns: `formula<'a> -> unit`	Printing parametrized by a function `pfn` to print atoms. tw : `TextWriter` pfn : `int -> 'a -> unit` Returns: `formula<'a> -> unit`
`fprint_latex_qformula tw pfn fm` Full Usage: `fprint_latex_qformula tw pfn fm` Parameters: tw : `TextWriter` pfn : `int -> 'a -> unit` fm : `formula<'a>`	Main toplevel latex printer. tw : `TextWriter` pfn : `int -> 'a -> unit` fm : `formula<'a>`
`fprint_qformula tw pfn fm` Full Usage: `fprint_qformula tw pfn fm` Parameters: tw : `TextWriter` pfn : `int -> 'a -> unit` fm : `formula<'a>`	Main toplevel printer. It just adds the guillemot-style quotations round the formula so that it looks like the quoted formulas we parse. tw : `TextWriter` pfn : `int -> 'a -> unit` fm : `formula<'a>` Note The quotations symbols `<<>>` for formulas have been replaced with `` that are more concise and cause less problems in writing documentation. Even if in F# there isn't an equivalent of OCaml's quotations expansions, it is convenient to keep quotation symbols to delimit formulas and terms to make it easier identifying.
`print_formula pfn fm` Full Usage: `print_formula pfn fm` Parameters: pfn : `int -> 'a -> unit` fm : `formula<'a>` Modifiers: inline Type parameters: 'a	Prints a formula `fm` using a function `pfn` to print atoms. pfn : `int -> 'a -> unit` fm : `formula<'a>`
`print_qformula pfn fm` Full Usage: `print_qformula pfn fm` Parameters: pfn : `int -> 'a -> unit` fm : `formula<'a>` Modifiers: inline Type parameters: 'a	Prints a formula `fm` using a function `pfn` to print atoms. pfn : `int -> 'a -> unit` fm : `formula<'a>`
`sprint_formula pfn fm` Full Usage: `sprint_formula pfn fm` Parameters: pfn : `int -> 'a -> unit` fm : `formula<'a>` Returns: `string` Modifiers: inline Type parameters: 'a	Returns a string representation of a formula `fm` using a function `pfn` to print atoms. pfn : `int -> 'a -> unit` fm : `formula<'a>` Returns: `string`
`sprint_qformula pfn fm` Full Usage: `sprint_qformula pfn fm` Parameters: pfn : `int -> 'a -> unit` fm : `formula<'a>` Returns: `string` Modifiers: inline Type parameters: 'a	Returns a string representation of a formula `fm` using a function `pfn` to print atoms. pfn : `int -> 'a -> unit` fm : `formula<'a>` Returns: `string`

Destructors

Functions and values

Function or value Description


                
                  
                    
                      antecedent fm

Full Usage: antecedent fm

Parameters:

fm : formula<'a> - The input formula.

Returns: formula<'a> The antecedent, if the input formula is an implication.
Modifiers: inline
Type parameters: 'a

Returns the antecedent of an implication.

fm : formula<'a>: The input formula.

Returns: formula<'a>: The antecedent, if the input formula is an implication.

Exception Thrown with message dest_imp, when fm is not an implication.

Example

 Imp (Atom "p", Atom "q") |> antecedent

Evaluates to Atom "p".

Example

 And (Atom "p", Atom "q") |> antecedent

Throws to System.Exception: dest_imp.


                
                  
                    
                      conjuncts fm

Full Usage: conjuncts fm

Parameters:

fm : formula<'a> - The supposed conjunction.

Returns: formula<'a> list The list of the conjuncts, if the input formula is a conjunction; otherwise a list containing the input formula unchanged.

Formula destructor for repeated conjunctions.

Recursively breaks apart repeated conjunctions \(p \land q \land r \cdots \) into the list of all the conjuncts \([p, q, r, \ldots]\).

fm : formula<'a>: The supposed conjunction.

Returns: formula<'a> list: The list of the conjuncts, if the input formula is a conjunction; otherwise a list containing the input formula unchanged.

Example

 And (And (Atom "p", Atom "q"), Atom "r")
 |> conjuncts

Evaluates to [Atom "p"; Atom "q"; Atom "r"].

Example

 Imp (Atom "a", Atom "b")
 |> conjuncts

Evaluates to [Imp (Atom "a", Atom "b")].


                
                  
                    
                      consequent fm

Full Usage: consequent fm

Parameters:

fm : formula<'a> - The input formula.

Returns: formula<'a> The consequent, if the input formula is an implication.
Modifiers: inline
Type parameters: 'a

Returns the consequent of an implication.

fm : formula<'a>: The input formula.

Returns: formula<'a>: The consequent, if the input formula is an implication.

Exception Thrown with message dest_imp, when fm is not an implication.

Example

 Imp (Atom "p", Atom "q") |> consequent

Evaluates to Atom "q".

Example

 And (Atom "p", Atom "q") |> consequent

Throws to System.Exception: dest_imp.


                
                  
                    
                      dest_and fm

Full Usage: dest_and fm

Parameters:

fm : formula<'a> - The supposed conjunction.

Returns: formula<'a> * formula<'a> The pair of the conjuncts, if the input formula is a conjunction.

Formula destructor for conjunctions.

It breaks apart a conjunction \(p \land q\) into the pair of its conjuncts \((p, q)\).

fm : formula<'a>: The supposed conjunction.

Returns: formula<'a> * formula<'a>: The pair of the conjuncts, if the input formula is a conjunction.

Exception Thrown with message dest_and, when fm is not a conjunction.

Example

 And (Atom "p", Atom "q") |> dest_and

Evaluates to (Atom "p", Atom "q").

Example

 Imp (Atom "p", Atom "q") |> dest_and

Throws to System.Exception: dest_and.


                
                  
                    
                      dest_iff fm

Full Usage: dest_iff fm

Parameters:

fm : formula<'a> - The supposed logical equivalence.

Returns: formula<'a> * formula<'a> The pair of the equivalence members, if the input formula is a logical equivalence.

Formula destructor for logical equivalences.

It breaks apart a logical equivalence \(p \Leftrightarrow q\) into the pair of its members \((p, q)\).

fm : formula<'a>: The supposed logical equivalence.

Returns: formula<'a> * formula<'a>: The pair of the equivalence members, if the input formula is a logical equivalence.

Exception Thrown with message dest_imp, when fm is not a logical equivalence.

Example

 Iff (Atom "p", Atom "q") |> dest_iff

Evaluates to (Atom "p", Atom "q").

Example

 Imp (Atom "p", Atom "q") |> dest_iff

Throws to System.Exception: dest_iff.


                
                  
                    
                      dest_imp fm

Full Usage: dest_imp fm

Parameters:

fm : formula<'a> - The supposed implication.

Returns: formula<'a> * formula<'a> The pair of the antecedent and consequent, if the input formula is an implication.

Formula destructor for implications.

It breaks apart an implications \(p \Rightarrow q\) into the pair of its antecedent and consequent \((p, q)\). See also: Formulas.antecedent, Formulas.consequent.

fm : formula<'a>: The supposed implication.

Returns: formula<'a> * formula<'a>: The pair of the antecedent and consequent, if the input formula is an implication.

Exception Thrown with message dest_imp, when fm is not an implication.

Example

 Imp (Atom "p", Atom "q") |> dest_imp

Evaluates to (Atom "p", Atom "q").

Example

 And (Atom "p", Atom "q") |> dest_imp

Throws to System.Exception: dest_imp.

Full Usage: dest_or fm

Parameters:

fm : formula<'a> - The supposed disjunction.

Returns: formula<'a> * formula<'a> The pair of the disjuncts, if the input formula is a disjunction.

Formula destructor for disjunctions.

It breaks apart a disjunction \(p \lor q\) into the pair of its conjuncts \((p, q)\).

fm : formula<'a>: The supposed disjunction.

Returns: formula<'a> * formula<'a>: The pair of the disjuncts, if the input formula is a disjunction.

Exception Thrown with message dest_or, when fm is not a disjunction.

Example

 Or (Atom "p", Atom "q") |> dest_or

Evaluates to (Atom "p", Atom "q").

Example

 Imp (Atom "p", Atom "q") |> dest_or

Throws to System.Exception: dest_or.


                
                  
                    
                      disjuncts fm

Full Usage: disjuncts fm

Parameters:

fm : formula<'a> - The supposed disjunction.

Returns: formula<'a> list The list of the disjuncts, if the input formula is a disjunction; otherwise a list containing the input formula unchanged.

Formula destructor for repeated disjunctions.

Recursively breaks apart repeated disjunctions \(p \lor q \lor r \cdots \) into the list of all the disjuncts \([p, q, r, \ldots]\).

fm : formula<'a>: The supposed disjunction.

Returns: formula<'a> list: The list of the disjuncts, if the input formula is a disjunction; otherwise a list containing the input formula unchanged.

Example

 Or (Or (Atom "p", Atom "q"), Atom "r")
 |> disjuncts

Evaluates to [Atom "p"; Atom "q"; Atom "r"].

Example

 Imp (Atom "a", Atom "b")
 |> disjuncts

Evaluates to [Imp (Atom "a", Atom "b")].


                
                  
                    
                      strip_quant fm

Full Usage: strip_quant fm

Parameters:

fm : formula<'a> - The supposed quantified formula.

Returns: string list * formula<'a> The pair of the list of its quantified variables and body, if the input formula is a universally quantified formula. If the formula is not a universally quantified one, the list of variables is empty.

Formula destructor for quantified formulas.

It breaks apart a quantified formula \(\forall xy\ldots z.\ p\) into a pair of the list of its quantified variables and body \(([x,y,\ldots,z], p)\).

fm : formula<'a>: The supposed quantified formula.

Returns: string list * formula<'a>: The pair of the list of its quantified variables and body, if the input formula is a universally quantified formula. If the formula is not a universally quantified one, the list of variables is empty.

Example

 Forall ("y", Forall ("x", Atom "p")) |> strip_quant

Evaluates to (["y"; "x"], Atom "p").

Example

 Atom "p" |> strip_quant

Evaluates to ([], Atom "p").

Constructors

Functions and values

Function or value	Description
`mk_and p q` Full Usage: `mk_and p q` Parameters: p : `formula<'a>` - The first formula to conjunct. q : `formula<'a>` - The second formula to conjunct. Returns: `formula<'a>` The conjunction of the input formulas. Modifiers: inline Type parameters: 'a	Constructs a conjunction. p : `formula<'a>` The first formula to conjunct. q : `formula<'a>` The second formula to conjunct. Returns: `formula<'a>` The conjunction of the input formulas. Example `mk_and (Atom "a") (Atom "b")` Evaluates to `And (Atom "a", Atom "b")`.
`mk_exists x p` Full Usage: `mk_exists x p` Parameters: x : `string` - The variable to bind. p : `formula<'a>` - The formula to bind. Returns: `formula<'a>` The `p` formula existentially quantified on `x`. Modifiers: inline Type parameters: 'a	Constructs an existential quantification. x : `string` The variable to bind. p : `formula<'a>` The formula to bind. Returns: `formula<'a>` The `p` formula existentially quantified on `x`. Example `mk_exists "x" (Atom "a")` Evaluates to `Exists ("x", Atom "a")`.
`mk_forall x p` Full Usage: `mk_forall x p` Parameters: x : `string` - The variable to bind. p : `formula<'a>` - The formula to bind. Returns: `formula<'a>` The `p` formula universally quantified on `x`. Modifiers: inline Type parameters: 'a	Constructs a universal quantification. x : `string` The variable to bind. p : `formula<'a>` The formula to bind. Returns: `formula<'a>` The `p` formula universally quantified on `x`. Example `mk_forall "x" (Atom "a")` Evaluates to `Forall ("x", Atom "a")`.
`mk_iff p q` Full Usage: `mk_iff p q` Parameters: p : `formula<'a>` - The first member of the equivalence to construct. q : `formula<'a>` - The second member of the equivalence to construct. Returns: `formula<'a>` The equivalence of `p` with `q`. Modifiers: inline Type parameters: 'a	Constructs a logical equivalence. p : `formula<'a>` The first member of the equivalence to construct. q : `formula<'a>` The second member of the equivalence to construct. Returns: `formula<'a>` The equivalence of `p` with `q`. Example `mk_iff (Atom "a") (Atom "b")` Evaluates to `Iff (Atom "a", Atom "b")`.
`mk_imp p q` Full Usage: `mk_imp p q` Parameters: p : `formula<'a>` - The antecedent of the implication to construct. q : `formula<'a>` - The consequent of the implication to construct. Returns: `formula<'a>` The implication with `p` as antecedent and `q` as consequent. Modifiers: inline Type parameters: 'a	Constructs an implication. p : `formula<'a>` The antecedent of the implication to construct. q : `formula<'a>` The consequent of the implication to construct. Returns: `formula<'a>` The implication with `p` as antecedent and `q` as consequent. Example `mk_imp (Atom "a") (Atom "b")` Evaluates to `Imp (Atom "a", Atom "b")`.
`mk_or p q` Full Usage: `mk_or p q` Parameters: p : `formula<'a>` - The first formula to disjunct. q : `formula<'a>` - The second formula to disjunct. Returns: `formula<'a>` The disjunction of the input formulas. Modifiers: inline Type parameters: 'a	Constructs a disjunction. p : `formula<'a>` The first formula to disjunct. q : `formula<'a>` The second formula to disjunct. Returns: `formula<'a>` The disjunction of the input formulas. Example `mk_or (Atom "a") (Atom "b")` Evaluates to `Or (Atom "a", Atom "b")`.

Syntax operations

Functions and values

Function or value	Description
`atom_union mapping fm` Full Usage: `atom_union mapping fm` Parameters: mapping : `'T -> 'U list` - The function to transform each attributes of the input formula's atoms into a sublist to be concatenated. fm : `formula<'T>` - The input formula. Returns: `'U list` The concatenation without duplicates of the transformed sublists.	For each attributes of the formula's atoms, applies the given function. Concatenates all the results and converts them to a set to remove duplicates. Except for the final removing of duplicates, it is for formula what ListModule.collect is for list. mapping : `'T -> 'U list` The function to transform each attributes of the input formula's atoms into a sublist to be concatenated. fm : `formula<'T>` The input formula. Returns: `'U list` The concatenation without duplicates of the transformed sublists. Example `And (Atom 1, And (Atom 2, And (Atom 3, Atom 4))) \|> atom_union (fun x -> [x])` Evaluates to `[1; 2; 3; 4]`. Example `And (Atom 1, And (Atom 2, And (Atom 3, Atom 4))) \|> atom_union (fun x -> [1..x]` The sample evaluates to `[1; 2; 3; 4]` and not to `[1; 1; 2; 1; 2; 3; 1; 2; 3; 4]` since duplicates are removed;
`onatoms f fm` Full Usage: `onatoms f fm` Parameters: f : `'a -> formula<'a>` - The function to apply to the attributes of the formula's atoms. fm : `formula<'a>` - The input formula. Returns: `formula<'a>` The formula with the atoms remapped by the function.	Applies a function `f` to all the attributes of the atoms in a formula `fm`, but otherwise leaves the structure unchanged. It can be used, for example, to perform systematic replacement of one particular atomic proposition by another formula. It is for formula what ListModule.map is for list. f : `'a -> formula<'a>` The function to apply to the attributes of the formula's atoms. fm : `formula<'a>` The input formula. Returns: `formula<'a>` The formula with the atoms remapped by the function. Example `And (Atom 1, Atom 2) \|> onatoms (fun x -> Atom (x * 5))` Evaluates to `And (Atom 5, Atom 10)`.
`overatoms folder fm state` Full Usage: `overatoms folder fm state` Parameters: folder : `'T -> 'State -> 'State` - The function to update the state given the input elements. fm : `formula<'T>` - The input formula. state : `'State` - The initial state. Returns: `'State` The final state value.	Applies a function to each attributes of formula's atoms, threading an accumulator argument through the computation. Take the third argument, and apply the function to it and the attribute of the first atom of the formula. Then feed this result into the function along with the second atom and so on. Return the final result. If the input function is `f` and the atoms are `Atom i0...Atom iN` then computes `f (... (f s i0) i1 ...) iN`. It is for formula what ListModule.fold is for list. folder : `'T -> 'State -> 'State` The function to update the state given the input elements. fm : `formula<'T>` The input formula. state : `'State` The initial state. Returns: `'State` The final state value. Note Although the inversion between the second and third arguments would seem to make this function similar to ListModule.foldBack, it actually corresponds to ListModule.fold because the folder function takes the accumulator as the first argument and the atom's argument as the second. Example `And (Atom 1, Atom 2) \|> fun fm -> overatoms (fun acc x -> acc + x) fm 0` val fm: obj Evaluates to `3`.

Calculemus

Formulas Module

Table of contents

Types

Parsing

Functions and values

Prettyprinting

Functions and values

Note

Destructors

Functions and values

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Example

Constructors

Functions and values

Example

Example

Example

Example

Example

Example

Syntax operations

Functions and values

Example

Example

Example

Note

Example