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

Literature.

[1] J. Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.

[CL] CL-TeX.

Chapter. Programs Operating on Symbolic Expressions.

The symbolic data structures are usually defined in the functional programming languages with the help of union types which can be readily arithmetized. We have seen already in one of the previous chapters an example of union type defining binary trees. In this chapter we will use another union types to arithmetize certain classes of symbolic expressions.

Section. Numeric Terms.

Numeric terms are symbolic expressions formed from variables and constants by the application of numeric binary operators of addition and multiplication.

Subsection. Arithmetization of Numeric Terms.

Constructors of numeric terms. Arithmetization of numeric expressions is done with the help of the following four pair constructors with pairwise different tags.

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}

Discrimination on the constructors of numeric terms. The pattern matching style of definitions of functions operating over the codes of numeric terms is obtained with conditionals called discrimination on the constructors of numeric terms. Example:

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

f (n^{•}) = ?

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

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

Numeric terms. Discrimination on the constructors of numeric terms is used in the definition of the predicate $Term (t)$ holding of the codes of numeric terms. The predicate is defined by course of values recursion. We refer to this kind of recursive definition as structural recursion on 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})

In the sequel we identify numeric terms with their codes and from now on we say the numeric term $t$ instead of the code $t$ of a numeric term.

[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

   Mt(At(Vt(1),Ct(2)),Vt(3)) = t

Subsection. Basic Operations and Predicates.

Size of numeric terms. The function $∣ t ∣$ yields the size of the numeric term $t$ , i.e. the number of operations including variables needed to construct the term. Example:

∣ (x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•} ∣ = 5

The function is defined by structural recursion on 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. (1 point) The function ${⟦ t ⟧}_{v}$ takes the numeric term $t$ and (the code of) the assignment $v$ and yields the value, i. e. denotation, of the term in the assignment. Example:

{⟦ (x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•} ⟧}_{10, 11, 12, 13, 0} = (11 + 2) \cdot 13

The function is defined by structural recursion on numeric terms.

{⟦ t ⟧}_{v} = ?

Free variables. The function $FV (t)$ yields the list of the indices of variables occurring in the numeric term $t$ . Example:

FV ((x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•}) = 1, 3, 0

The function is defined by structural recursion on numeric terms.

FV (t) = ?

Subsection. Additive Normal Form.

Multiplicative terms. The predicate $Mterm (t)$ is holding of multiplicative terms. These are numeric terms formed from variables and constants by the application of multiplication. Example:

Mterm (x_{1}^{•} \times^{•} 2^{•} \times^{•} x_{3}^{•}) \land \neg Mterm ((x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•})

The predicate is defined by structural recursion on numeric terms.

Mterm (x_{i}^{•})

Mterm (n^{•})

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

Terms in additive normal form. The predicate $Anf (t)$ is holding of terms in additive normal form. These are either multiplicative terms or addition of two numeric terms in additive normal form. Example:

Anf (x_{1}^{•} \times^{•} x_{3}^{•} +^{•} 2^{•} \times^{•} x_{3}^{•}) \land \neg Anf ((x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•})

The predicate is defined by structural recursion on numeric terms.

Anf (t) \leftarrow Mterm (t)

Anf (t) \leftarrow \neg Mterm (t) \land t = t_{1} +^{•} t_{2} \land Anf (t_{1}) \land Anf (t_{2})

Exercise. Define the function $Mul_ma (s, t)$ such that

Term (s) \land Term (t) \to Term Mul_ma (s, t)

Mterm (s) \land Term (t) \land Anf (t) \to Anf Mul_ma (s, t)

Term (s) \land Term (t) \to {⟦ Mul_ma (s, t) ⟧}_{vs} = {⟦ s \times^{•} t ⟧}_{vs}

Mul_ma (s, t) = ?

Exercise. Define the function $Mul_aa (s, t)$ such that

Term (s) \land Term (t) \to Term Mul_aa (s, t)

Term (s) \land Anf (s) \land Term (t) \land Anf (t) \to Anf Mul_aa (s, t)

Term (s) \land Term (t) \to {⟦ Mul_aa (s, t) ⟧}_{vs} = {⟦ s \times^{•} t ⟧}_{vs}

Mul_aa (s, t) = ?

Rearranging terms into additive normal form. (2 points) Define the function $Anf_from (t)$ such that

Term (t) \to Term Anf_from (t)

Term (t) \to Anf Anf_from (t)

Term (t) \to {⟦ Anf_from (t) ⟧}_{vs} = {⟦ t ⟧}_{vs}

Anf_from (t) = ?

Subsection. Left Associated Addition.

In this part we give an example of a program which goes beyond structural recursion. We consider the problem of rearranging numeric terms so that the additions which they contain are associated to left.

Terms with left associated addition. The predicate $Lassoc (t)$ is holding of numeric terms with left associated addition. Example:

Lassoc (x_{1}^{•} +^{•} x_{2}^{•} +^{•} x_{3}^{•}) \land \neg Lassoc (x_{1}^{•} +^{•} (x_{2}^{•} +^{•} x_{3}^{•}))

The predicate is defined by structural recursion on numeric terms.

Lassoc (x_{i}^{•})

Lassoc (n^{•})

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

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

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

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

Rearranging terms into expressions with left associated addition. (1 point) Define the function $Lassoc_from (t)$ such that

Term (t) \to Term Lassoc_from (t)

Term (t) \to Lassoc Lassoc_from (t)

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

Do not use auxiliary functions!

Hint. Put

Lassoc_from (t_{1} +^{•} (t_{2} +^{•} t_{3})) = Lassoc_from (t_{1} +^{•} t_{2} +^{•} t_{3})

Define $Lassoc_from (t)$ by recursion with the measure $μ [t]$ :

μ [x_{i}^{•}] = 0

μ [n^{•}] = 0

μ [t_{1} \times^{•} t_{2}] = 0

μ [t_{1} +^{•} t_{2}] = μ [t_{1}] + 2 \cdot μ [t_{2}] + 1

Lassoc_from (t) = ?

Subsection. Postfix Machine.

Numeric terms are compiled into programs of a postfix machine and then the programs are executed.

Instructions. The instructions of the postfix machine are defined with the help of four pair constructors with pairwise different tags.

LOAD (i) = 0, i

PUSH (n) = 1, n

ADD = 2, 0

MULT = 3, 0

The predicate $Instr (i)$ holding of instructions of the postfix machine is defined as follows.

Instr LOAD (i) \leftarrow N (i)

Instr PUSH (n) \leftarrow N (n)

Instr (ADD)

Instr (MULT)

Programs. The predicate $Program (p)$ holding of programs of the postfix machine is defined by list recursion.

Program (0)

Program (i, p) \leftarrow Instr (i) \land Program (p)

[CL] Formatting the output. Use the format $Program$ to display numbers as programs. Try out the following simple queries

   4723455160 = p:Program

   (0,1),(1,2),(2,0),(0,3),(3,0),0 = p:Program

   Vi(1),Ci(2),Ai,Vi(3),Mi,0 = p

Compilation. (1 point) Numeric terms are compiled into programs of the postfix machine with the help of the operation $Cmp (t)$ :

Term (t) \to Program Cmp (t)

Example:

Cmp ((x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•}) = LOAD (1), PUSH (2), ADD, LOAD (3), MULT, 0

The compilation function is defined by structural recursion on numeric terms.

Cmp (t) = ?

One-step evaluation. (1 point) The operation of the postfix machine itself is described by the ternary function $Run (p, v, s)$ , where $p$ is a program, $v$ is an assignment (environment), and $s$ is a list of values (I/O stack). Specification:

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

Invariant:

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

The function $Run (p, v, s)$ is defined by structural recursion on the program $p$ .

Run (p, v, s) = ?

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

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

Example:

Decmp (LOAD (1), PUSH (2), ADD, LOAD (3), MULT, 0) = (x_{1}^{•} +^{•} 2^{•}) \times^{•} x_{3}^{•}

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, t, s) = ?

Decmp (p) = ?