Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

[CL] CL-TeX.

Chapter. Programs Operating on Symbolic Expressions.

Section. Numeric Terms.

Subsection. Arithmetization of Numeric Terms.

Constructors of numeric terms.

x_{i}^{•} = 0, i

n^{•} = 1, n

t_{1} +^{•} t_{2} = 2, t_{1}, t_{2}

t_{1} \times^{•} t_{2} = 3, t_{1}, t_{2}

[CL] Discrimination on the constructors of numeric terms. Example(s):

f (x_{i}^{•}) = ?

f (n^{•}) = ?

f (t_{1} +^{•} t_{2}) = ?

f (t_{1} \times^{•} t_{2}) = ?

Numeric terms.

Term (x_{i}^{•}) \leftarrow N (i)

Term (n^{•}) \leftarrow N (n)

Term (t_{1} +^{•} t_{2}) \leftarrow Term (t_{1}) \land Term (t_{2})

Term (t_{1} \times^{•} t_{2}) \leftarrow Term (t_{1}) \land Term (t_{2})

[CL] Formatting the output. Use the format $Term$ to display numbers as numeric terms. Try out the following simple queries

   98041654 = t:Term

   3,(2,(0,1),1,2),0,3 = t:Term

[CL] Structural case analysis on numeric terms. Syntax:

case Term ; <term>

Example(s):

$case Term; t$
$\frac{Term (t)}{t = x_{i}^{•} ∣ t = n^{•} ∣ t = t_{1} +^{•} t_{2} \land Term (t_{1}) \land Term (t_{2}) ∣ t = t_{1} \times^{•} t_{2} \land Term (t_{1}) \land Term (t_{2})}$
where $i$ , $n$ , $t_{1}$ and $t_{2}$ are new variables (eigen-variables).

Structural induction on numeric terms. Show that the principle of structural induction over numeric terms is admissible in Peano arithmetic.

Remark. Prove the claim for the special case in the following theory.

[CL] Hint. Reduce structural induction on $t$ to course of values induction with measure $| t |_{p}$ . Recall that the pair size function $| x |_{p}$ , written as |x|, is defined in the module Standard.

φ [x_{i}^{•}]

φ [n^{•}]

φ [t_{1}] \land φ [t_{2}] \to φ [t_{1} +^{•} t_{2}]

φ [t_{1}] \land φ [t_{2}] \to φ [t_{1} \times^{•} t_{2}]

Term (t) \to φ [t]

[CL] Structural induction on numeric terms. Syntax:

ind Term ; <variable> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

$ind Term; t$
$\frac{Term (t) \to φ [t] *}{φ [x_{i}^{•}] * ∣ φ [n^{•}] * ∣ φ [t_{1}] \land φ [t_{2}] \to φ [t_{1} +^{•} t_{2}] * ∣ φ [t_{1}] \land φ [t_{2}] \to φ [t_{1} \times^{•} t_{2}] *}$
where $i$ , $n$ , $t_{1}$ and $t_{2}$ are new variables (eigen-variables).
$ind Term; t; a$
$\frac{Term (t) \to φ [t] *}{φ [x_{i}^{•}] * ∣ φ [n^{•}] * ∣ \forall a φ [t_{1}] \land \forall a φ [t_{2}] \to φ [t_{1} +^{•} t_{2}] * ∣ \forall a φ [t_{1}] \land \forall a φ [t_{2}] \to φ [t_{1} \times^{•} t_{2}] *}$
where $i$ , $n$ , $t_{1}$ and $t_{2}$ are new variables (eigen-variables).

[CL] Structural induction on numeric terms (2nd form). Syntax:

ind* Term ; <variable> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

$ind* Term; t$
$\frac{Term (t) \to φ [t] *}{φ [x_{i}^{•}] * ∣ φ [n^{•}] * ∣ Term (t_{1}) \land φ [t_{1}] \land Term (t_{2}) \land φ [t_{2}] \to φ [t_{1} +^{•} t_{2}] * ∣ Term (t_{1}) \land φ [t_{1}] \land Term (t_{2}) \land φ [t_{2}] \to φ [t_{1} \times^{•} t_{2}] *}$
where $i$ , $n$ , $t_{1}$ and $t_{2}$ are new variables (eigen-variables).
$ind* Term; t; a$
$\frac{Term (t) \to φ [t] *}{φ [x_{i}^{•}] * ∣ φ [n^{•}] * ∣ Term (t_{1}) \land \forall a φ [t_{1}] \land Term (t_{2}) \land \forall a φ [t_{2}] \to φ [t_{1} +^{•} t_{2}] * ∣ Term (t_{1}) \land \forall a φ [t_{1}] \land Term (t_{2}) \land \forall a φ [t_{2}] \to φ [t_{1} \times^{•} t_{2}] *}$
where $i$ , $n$ , $t_{1}$ and $t_{2}$ are new variables (eigen-variables).

Subsection. Basic Operations and Predicates.

Size of numeric terms.

∣ x_{i}^{•} ∣ = 1

∣ n^{•} ∣ = 1

∣ t_{1} +^{•} t_{2} ∣ = ∣ t_{1} ∣ + ∣ t_{2} ∣ + 1

∣ t_{1} \times^{•} t_{2} ∣ = ∣ t_{1} ∣ + ∣ t_{2} ∣ + 1

Denotation of numeric terms.

{⟦ t ⟧}_{v} = ?

Free variables.

FV (t) = ?

Coincidence of assignments.

v_{1} \equiv v_{2} [is] \leftrightarrow \forall i (i &CLin; is \to v_{1} [i] = v_{2} [i])

Exercise. Prove

v_{1} \equiv v_{2} [0]

v_{1} \equiv v_{2} [i, is] \leftrightarrow v_{1} [i] = v_{2} [i] \land v_{1} \equiv v_{2} [is]

[CL] Hint. Use the pseudo-command open to force opening the explicit definition of the predicates $v_{1} \equiv v_{2} [is]$ .

v_{1} \equiv v_{2} [0]

v_{1} \equiv v_{2} [i, is] \leftrightarrow v_{1} [i] = v_{2} [i] \land v_{1} \equiv v_{2} [is]

Exercise. Prove

Term (t) \land v_{1} \equiv v_{2} [FV (t)] \to {⟦ t ⟧}_{v_{1}} = {⟦ t ⟧}_{v_{2}}

Term (t) \land v_{1} \equiv v_{2} [FV (t)] \to {⟦ t ⟧}_{v_{1}} = {⟦ t ⟧}_{v_{2}}

Subsection. Postfix Machine.

Instructions.

LOAD (i) = 0, i

PUSH (n) = 1, n

ADD = 2, 0

MULT = 3, 0

Instr LOAD (i) \leftarrow N (i)

Instr PUSH (n) \leftarrow N (n)

Instr (ADD)

Instr (MULT)

Programs.

Program (p) \leftrightarrow ?

Compilation.

Cmp (t) = ?

Exercise. Prove

Term (t) \to Program Cmp (t)

Term (t) \to Program Cmp (t)

One-step evaluation.

Run (p, v, s) = ?

Exercise. Prove

Term (t) \to {⟦ t ⟧}_{v} = Run (Cmp (t), v, 0)

Term (t) \to {⟦ t ⟧}_{v} = Run (Cmp (t), v, 0)

Decompilation. Define the function $Decmp (t)$ such that

Term (t) \to Decmp Cmp (t) = t

Verify your implementation!

Hint. Define first an auxiliary binary function $f (p, s)$ such that

Term (t) \to f (Cmp (t) \oplus p, s) = f (p, t, s)

f (p, s) = ?

Decmp (p) = ?

Term (t) \to f (Cmp (t) \oplus p, s) = f (p, t, s)

Term (t) \to Decmp Cmp (t) = t

Subsection. Additional Problems.

Terms with left associated addition.

Lassoc (x_{i}^{•})

Lassoc (n^{•})

Lassoc (t +^{•} x_{i}^{•}) \leftarrow Lassoc (t)

Lassoc (t +^{•} n^{•}) \leftarrow Lassoc (t)

Lassoc (t +^{•} t_{1} \times^{•} t_{2}) \leftarrow Lassoc (t)

Lassoc (t_{1} \times^{•} t_{2})

Rearranging terms into expressions with left associated addition.

f (t) = ?

Remark. Note that the function $f (t)$ is defined by recursion with a suitable measure $μ [t]$ :

μ [t] = ?

μ [t_{1}] < μ [t_{1} +^{•} x_{i}^{•}]

μ [t_{1}] < μ [t_{1} +^{•} n^{•}]

μ [t_{1}] < μ [t_{1} +^{•} t_{2} \times^{•} t_{3}]

μ [t_{1} +^{•} t_{2} +^{•} t_{3}] < μ [t_{1} +^{•} (t_{2} +^{•} t_{3})]

Exercise. Prove

Term (t) \to Term f (t)

Term (t) \to Lassoc f (t)

Term (t) \to {⟦ f (t) ⟧}_{v} = {⟦ t ⟧}_{v}

Term (t) \to ∣ f (t) ∣ = ∣ t ∣

Term (t) \to Term f (t)

Term (t) \to Lassoc f (t)

Term (t) \to {⟦ f (t) ⟧}_{v} = {⟦ t ⟧}_{v}

Term (t) \to ∣ f (t) ∣ = ∣ t ∣