[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

### 2.7.5 How `avram` Thinks

The definitions in the standard `silly` library pertaining to the basic properties of the operator can provide a good intuitive illustration of how computations are performed by `avram`. This task is approached in the guise of a few trivial correctness proofs about them. Conveniently, as an infeasibly small language, `silly` is an ideal candidate for analysis by formal methods.

Technically the semantic function [[…]] has not been defined on identifiers, but we can easily extend it to them by stipulating that the meaning of an identifier `x` is the meaning of the program `main = x` when linked with a library containing the declaration of `x`, where `main` is an identifier not appearing elsewhere in the library.

With this idea in mind, the following “theorems” can be stated, all of which have a similar proof. The variables x and y stand for any tree, and the variable f stands for any tree other than `nil`.

T0

  [[`identity`]] `x` = `x`

T1

  [[`left`]] `(x,y)` = `x`

T2

  [[`right`]] `(x,y)` = `y`

T4

  [[`meta`]] `(f,x)` = `f (f,x)`

T5

  [[`constant_nil`]] `x` = `nil`

Replacing each identifier with its defining expression directly demonstrates a logical equivalence between the relevant theorem and one of the basic operator properties postulated in A Minimal Set of Properties.

For more of a challenge, it is possible to prove the next theorem.

T6

  For non-`nil` `f` and `g`, ([[`couple`]] `(f,g)`) `x` = `(f x,g x)`

The proof is a routine calculation. Beware of the distinction between the mathematical `nil` and the `silly` identifier `nil`.

       ([[couple]] (f,g)) x =  ([[((((left,nil),constant_nil),nil),right)]] (f,g)) x

    by substitution of couple with its definition in the standard library

       = ((((([[left]],[[nil]]),[[constant_nil]]),[[nil]]),[[right]]) (f,g)) x

    by definition of the semantic function [[…]] regarding pairs

       = ((((([[left]],[[()]]),[[constant_nil]]),[[()]]),[[right]]) (f,g)) x

    by substitution of nil from its definition in the standard library

       = ((((([[left]],nil),[[constant_nil]]),nil),[[right]]) (f,g)) x

    by definition of the semantic function in the case of [[()]]

       = (([[left]] (f,g),[[constant_nil]] (f,g)),[[right]] (f,g)) x

    by property P6 (twice)

       = ((f,nil),g) x

    by theorems T1, T2, and T5

       = (f x,g x)

    by property P6 again.

Something to observe about this proof is that it might just as well have been done automatically. Every step is either the substitution of an identifier or a pattern match against existing theorems and properties of the operator. Another thing to note is that the use of identifiers and previously established theorems helps to make the proof human readable, but is not a logical necessity. An equivalent proof could have been expressed entirely in terms of the properties of the operator. If one envisions a proof like this being performed blindly and mechanically, without the running commentary or other amenities, that would not be a bad way of thinking about what takes place when `avram` executes virtual code.

Three more theorems have similar proofs. For non-`nil` trees `p`, `f` and `g`, and any trees `x` and `k`:

T7

  ([[`compose`]] `(f,g)`) x = f g x

T8

  ([[`constant`]] `k`) x = k

T9

  ([[`conditional`]] `(p,(f,g)`) x = `f x` if `p x` is non-`nil`, but `g x` if `p x` = `nil`

The proofs of these theorems are routine calculations analogous to the proof of T6. Here is a proof of theorem T7 for good measure.

       ([[compose]] (f,g)) x = ([[couple(identity,constant_nil)]] (f,g)) x

by substitution of `compose` with its definition in the standard library

       = (([[couple]] ([[identity]],[[constant_nil]]))(f,g)) x

    by definition of the semantic function

       = ([[identity]] (f,g),[[constant_nil]] (f,g)) x

    by theorem T6

       = ((f,g),nil) x

    by theorems T0 and T5

       = f g x

    by property P5 of the operator.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

This document was generated on November 8, 2012 using texi2html 1.82.