Calculemus

Equal Module

Namespace: Calculemus
Assembly: Calculemus.dll

Naive equality axiomatization.

Table of contents

Syntax operation

Functions and values

Function or value Description

dest_eq fm

Full Usage: dest_eq fm

Parameters:
Returns: term * term The pair of the LHS and RHS terms of the equation.

Formula destructor for equations.

fm : formula<fol>

The input formula.

Returns: term * term

The pair of the LHS and RHS terms of the equation.

Exception Thrown with message dest_eq: not an equation when the input formula is not an equation.
Example 

 dest_eq !!"f(x) = y"
Evaluates to (``f(x)``,``y``).

Example 

 dest_eq !!"P(x) <=> Q(y)"
Throws System.Exception: dest_eq: not an equation.

is_eq fm

Full Usage: is_eq fm

Parameters:
Returns: bool true, if the input formula is an equation; otherwise, false.

Tests if a formula is an equation.

fm : formula<fol>

The input formula.

Returns: bool

true, if the input formula is an equation; otherwise, false.

Example 

 !!"x = y"
 |> is_eq
Evaluates to true.

Example

Logical equations are not equations. 

 !!"P(x) <=> Q(x)"
 |> is_eq
Evaluates to false.

lhs eq

Full Usage: lhs eq

Parameters:
Returns: term The LHS term of the equation.

Returns the LHS term of an equation.

eq : formula<fol>

The input equation.

Returns: term

The LHS term of the equation.

Exception Thrown with message dest_eq: not an equation when the input formula is not an equation.
Example 

 lhs !!"f(x) = y"
Evaluates to ``f(x)``.

Example 

 lhs !!"P(x) <=> Q(y)"
Throws System.Exception: dest_eq: not an equation.

mk_eq s t

Full Usage: mk_eq s t

Parameters:
    s : term - The first input term.
    t : term - The second input term.

Returns: formula<fol> The equation of the input terms.

Constructs an equation.

s : term

The first input term.

t : term

The second input term.

Returns: formula<fol>

The equation of the input terms.

Example 

 mk_eq !!!"f(x)" !!!"y"
Evaluates to `f(x) = y`.

predicates fm

Full Usage: predicates fm

Parameters:
Returns: (string * int) list The list of name-arity pairs of the predicates in the formula.

Returns the predicates present in the input formula fm.

fm : formula<fol>

The input formula.

Returns: (string * int) list

The list of name-arity pairs of the predicates in the formula.

Example 

 predicates !!"x + 1 > 0 /\ f(z) > g(z,i)"
Evaluates to [(">", 2)].

rhs eq

Full Usage: rhs eq

Parameters:
Returns: term The RHS term of the equation.

Returns the RHS term of an equation.

eq : formula<fol>

The input equation.

Returns: term

The RHS term of the equation.

Exception Thrown with message dest_eq: not an equation when the input formula is not an equation.
Example 

 rhs !!"f(x) = y"
Evaluates to ``y``.

Example 

 rhs !!"P(x) <=> Q(y)"
Throws System.Exception: dest_eq: not an equation.

Equality axioms

Functions and values

Function or value Description

equalitize fm

Full Usage: equalitize fm

Parameters:
Returns: formula<fol> The input formula itself if it doesn't involve equality at all; otherwise, the implication of the input formula from its equality axioms.

Returns the implication of the input formula from its equality axioms.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The input formula itself if it doesn't involve equality at all; otherwise, the implication of the input formula from its equality axioms.

Example 

 !! @"(forall x. f(x) ==> g(x)) /\
      (exists x. f(x)) /\
      (forall x y. g(x) /\ g(y) ==> x = y)
      ==> forall y. g(y) ==> f(y)"
 |> equalitize
 |> sprint_fol_formula
Evaluates to 
 "(forall x. x = x) /\ 
  (forall x y z. x = y /\ x = z ==> y = z) /\ 
  (forall x1 y1. x1 = y1 ==> f(x1) ==> f(y1)) /\ 
  (forall x1 y1. x1 = y1 ==> g(x1) ==> g(y1)) ==> 
  (forall x. f(x) ==> g(x)) /\ 
  (exists x. f(x)) /\ 
  (forall x y. g(x) /\ g(y) ==> x = y) 
  ==> (forall y. g(y) ==> f(y))"

Example 

 equalitize !!"P(x) <=> Q(y)"
Evaluates to `P(x) <=> Q(y)`.

equivalence_axioms

Full Usage: equivalence_axioms

Returns: formula<fol> list The list of the equivalence axioms.

Returns the list of equivalence axioms.

Reflexivity and a variation of transitivity: \begin{align*} &\forall x.\ x = x \\ &\forall x\ y\ z.\ x = y \land x = z \Rightarrow y = z \end{align*} Symmetry follows by instantiating that axiom so that \(x\) and \(z\) are the same, then using reflexivity.

Returns: formula<fol> list

The list of the equivalence axioms.

function_congruence (f, n)

Full Usage: function_congruence (f, n)

Parameters:
    f : string - The function symbol name.
    n : int - The function arity.

Returns: formula<fol> list The list with the congruence axiom for the given function as the only element, if n > 0; otherwise, the empty list.

Returns the congruence axiom for the given function.

f : string

The function symbol name.

n : int

The function arity.

Returns: formula<fol> list

The list with the congruence axiom for the given function as the only element, if n > 0; otherwise, the empty list.

Example 

 function_congruence ("f",2)
Evaluates to [`forall x1 x2 y1 y2. x1 = y1 /\ x2 = y2 ==> f(x1,x2) = f(y1,y2)`].

Example 

 function_congruence ("f",0)
Evaluates to [].

predicate_congruence (p, n)

Full Usage: predicate_congruence (p, n)

Parameters:
    p : string - The predicate symbol name.
    n : int - The predicate arity.

Returns: formula<fol> list The list with the congruence axiom for the given predicate as the only element, if n > 0; otherwise, the empty list.

Returns the congruence axiom for the given predicate.

p : string

The predicate symbol name.

n : int

The predicate arity.

Returns: formula<fol> list

The list with the congruence axiom for the given predicate as the only element, if n > 0; otherwise, the empty list.

Example 

 predicate_congruence ("P",3)
Evaluates to [`forall x1 x2 x3 y1 y2 y3. x1 = y1 /\ x2 = y2 /\ x3 = y3 ==> P(x1,x2,x3) ==> P(y1,y2,y3)`].

Example 

 predicate_congruence ("P",0)
Evaluates to [].