Novell Home

OpenEd - Lab 7

From Developer Community

[ C:TaPiC ]

Lab 1 Lab 2 Lab 3 Lab 4 Lab 5 Lab 6 Lab 7 Lab 8

[edit]

Recursive functions and register machines

[edit]

What's the point?

Proving programs correct can seem intractable. Can we by starting with a very simple computing device and a simple language build up programs that are correct by construction through proof?

For example consider that we want to create a program / machine to add two numbers: 

σ(R1) = m, σ(R2) = n
// program.
σ(R1) = m + n

Can we prove the following? 

σ(R1) = m, σ(R2) = n
  REG_1 <- R1
  REG_2 <- R2
    0 STOP
    1 TSTZ REG_2 0 DEC REG_2 2
    2 INC REG_1 1
  R1 <- REG_1
σ(R1) = m + n

The following definition is take from Johnstone (1987).

[edit]

Definition of a register machine

A register machine has a sequence of registers R1, R2, . . . , each of which may at any time hold an arbitrary natural number. A program for the machine is defined by specifying a finitie number of states S0, S1. . . . , Sn , together with, for each i > 0, an instruction to be carried out whenever the machine is in state Si . (S0 is the terminal state; on reaching it, the machine 'switches itself off'.) These instruction are of two kinds:

  1. add 1 ro register Ri , and move to state Sk
  2. test whether Ri holds the number 0: if it does, move to state Sl otherwise subtract 1 from it and move to state Sk .
[edit]

A language 

   <program> ::= <stop-state> (<label><state>)*
<stop-state> ::= 0 STOP
     <state> ::= <inc-state> | <tstz-state>
 <inc-state> ::= INC <reg> <next-state>
<tstz-state> ::= TSTZ <reg> <label> DEC <reg> <label>
       <reg> ::= REG_<number>
     <label> ::= <number>
[edit]

Empty REG_0

The following program will empty the contents of register 0. 

0 STOP
1 TSTZ REG_0 0 DEC REG_0 1
[edit]

Move REG_1 into REG_0

The following program will move the contents of REG_1 into REG_0 emptying the contents of RGE_1 in the process. 

0 STOP
1 TSTZ REG_0 2 DEC REG_0 1
2 TSTZ REG_1 0 DEC REG_1 3
3 INC REG_0 2
[edit]

Copy REG_1 into REG_0

The following program wil copy the contents of register 1 into register 0. At the end of the excution register 0 and register 1 will contain the same value. 

0 STOP
1 TSTZ REG_0 2 DEC REG_0 1
2 TSTZ REG_2 3 DEC REG_2 2
3 TSTZ REG_1 5 DEC REG_1 4
4 INC REG_2 3
5 TSTZ REG_2 0 DEC REG_0 6
6 INC REG_0 7
7 INC REG_1 5
[edit]

Semantics and Proofs

This is the first attempt at providing a semantics for the machines described above.

  • The semantics for a program is a function from state to state.
    • [[P]] : Σ → Σ
  • A state is a function from identifiers to natural numbers.
    • Σ : Id → N

[[P]] is taken as the graph of the program and contrasts with the operational semantics described below.

When a program executes it will move through program states.

  • A program state consists of:
    • a program
    • a current instruction
    • and the current storage state
  • A program state has the signature:
    • PS : P × N × Σ
  • A program is a function from natural numbers to instructions:
  • P : N → I
  • An instruction is a pair of functions.
    • The first function is a function from storage state to natural numbers
    • The second function is a function from storage state to storage state
  • An instruction has the signature:
    • I : Σ → N × Σ → Σ


[edit]

The delta function

The delta function at the level of instructions is defined as follows:

  • Δ(p, σ) = Δ(p, 1, σ)
  • Δ(p, n, σ) = Δ(p, Δn,0(σ), Δn,1(σ))
  • Δ(p, 0, σ) = σ

TODO: fuller explanation of the above.

Retrieved from "http://developer.novell.com/wiki/index.php/OpenEd_-_Lab_7"

Novell® Making IT Work As One™

© 2009 Novell, Inc. All Rights Reserved.