User:Thepigdog/Relational model of imperative programming

The relational model of imperative programming describes how time and state may be managed in relational programming, and how imperative programming may be represented within relational programming. The goals are,

• Represent of an imperative program within a relational program.
• Logical transformations of imperative programs.
• Time based interaction with other systems and services in relational programs.

This allows code refactoring of an imperative program into relational program while preserving its functionality.

A relational program must interact with its environment. To do this in a sound manner the program must be able to obtain the current time without pre-determining the execution order.

Introduction

Relational programming languages are based on the objective mathematical model where the world being described is separate from the method of description, and time is a dimension. Relational programs gain from this the freedom to be executed in any order. However this places some constraints on the interaction of a program with its environment.

The state of an imperative program can be turned into a mathematical object by parameterizing it with time. The state at a particular time is a well defined object with a single value. The current state may be obtained using the current time.

A relational program may be written which regards time as a dimension, provided it has access to the current time. The current time may be accessed from a list of times, where each time is current at the time it is read from the list.

Current time

Allowing a relational program access to the current time, without pre-determining the order of execution is difficult. The natural way to represent obtaining the current time is to ask a clock. The clock returns the time and, because it is stateless, returns the next clock. The clock implements a list of times.

However, as well as being inconvenient, passing the clock around unnecessarily pre-determines the order of execution. An example is when logging messages as a record of what the program as done. Log messages need to be tagged with the time, which requires access to the clock. But access to the clock requires that the next clock to be passed on to the next use, which pre-determines the order of execution. But in fact the requirement was to log the order of execution, not determine it.

Branching clocks solve this problem.

Working with legacy programs

Imperative programs are characterized by having implicit state. An imperative program describes a series of changes to the state, executed in a defined order.

Most programs are written in imperative programming languages. In order to successfully transform large imperative programs, a flexible system is needed that allows incremental changes to be made. Large scale changes to a big imperative program may cause bugs which are hard to track down and correct. Small changes may be introduced and any bugs found may be attributed to individual changes.

Roles

A role is an implicit parameter to a function, identified by a name, whose value is requested from its calling context. If the calling context, within another function definition, does not provide the value, then the role becomes a request of any call to the function. The request is passed up the calling hierarchy until the value is provided.

The purpose of roles is to provide an implicit mechanism for constructing parameter parsing through a hierarchy of multiple function calls without explicitly defining the actual or the formal parameter. The role requests the value and the parameter parsing to transport the value is constructed automatically by meta programming.

This has advantages,

• The calling sequence is constructed automatically, eliminating bugs caused by manual construction.
• The reader of the program is not distracted by parameters that are not needed locally in the function.
• A change to a program may introduce the need for a value in a function, without adding all the parameter passing needed to deliver the value.

Role pre-processor

A role pre-processor for a language processes source text and identifies two meta functions,

• provide - Identifies the value for later use.
• request - Requests the creation of all the parameter passing needed to get the value here.

The pre-processor implements a request by adding an extra formal parameter to a function for each value requested in it. The parameter will be used to pass in the requested value. Then for each function call, add the actual parameter and implicitly regard that value as requested in its containing function.

Recursively implement requests in that way until a provide meta function is found for the same name.

The pre-processor could obtain the type of the variable from the provided variable. Alternately the provide meta function could give the type.

Example

In this example, someParameter is provided in the main function, but is needed in MyDetailedLowLevelCalculation.

Making someParameter a global variable would make it harder to later parameterize any of the functions to be called with different values.

Another alternative would be to create a class as a container for all my methods. someParameter could be a member variable which is populated in the constructor. But in a more complex example these methods may already be across different classes. I may end up parsing the value between classes, to get it where I want it.

The most direct and flexible approach is to parse the value as a parameter, but as well as being distracting for the reader, and adding additional parameters to each call, the developer has to do more work, all of which may need to be removed later if the requirements change.

In this example a role-preprocessor adds the extra parameters. The text is show after the pre-processor has been run with added text surrounded by comments as in,

 /* Role processor add  */ someParameter, logger /* end add */

In the code ... represents code omitted for the sake of brevity. The example code is,

#include ...
#define provide(x, t) // Role processing directive does not do anything here
#define request(x)

class ObjectToBeProcessed;
void MyProcessing();
void MyProcessObject();
double MyDetailedLowLevelCalculation(double v);

void main(int argc, char **argv)
{
  Logger logger;
  double someParameter = atof(argv[0]);
  ...;
  provide(someParameter, double);    // I have the value someParameter, if anyone wants it.
  provide(logger, Logger &);         // Also I am providing the logger.
  MyProcessing( /* Role processor add */ someParameter, logger /* end add */);
}

void MyProcessing( /* Role processor add */ double someParameter, Logger &logger /* end add */)
{
  ...
  {
    ObjectToBeProcessed *o = ...;
    MyProcessObject(/* Role processor add */ someParameter, logger,  /* end add */ o);
  }
  ...
}
  
void MyProcessObject( /* Role processor add*/ double someParameter, Logger &logger  /* end add */)
{
  ...
  double myValue = ...;
  double value = MyDetailedLowLevelCalculation( /* Role processor add */ someParameter,  /* end add */ myValue);

  // Add logging here, for debugging purposes.  I might take it out later.
  // The logger would normally be a global variable, but again this reduces flexibility.
  request(logger); 
  logger << "MyProcessObject: result = " << to_string(value); 
  ...
}

double MyDetailedLowLevelCalculation( /* Role processor add */ double someParameter,  /* end add */ double v)
{
  // Oops, now I need some parameter.
  request(someParameter); // Please construct all the parameter passing to get the value here.
  // See the code added by the role processor.
  return v * someParameter; // Some calculation
}

A role pre-processor would be hard to implement in a language without meta processing functionality, because the pre-processor would need to parse and understand at least some of the syntax of the language. Identifying the type of the variable would be challenging.

However a role pre-processor may be written as a few rules in a language supporting meta-programming.

Roles in lambda calculus

Named lambda expression is producer.

$\lambda _{x}y.z$

Request is

$\gamma _{x}y.z$

Axioms

$\lambda _{x}y.\gamma _{x}v.z=\lambda _{x}y.z[v:=y]$

$p\neq q\to \lambda _{p}y.\gamma _{q}v.z=\gamma _{q}v.\lambda _{p}y.z$

Alpha rename applies to $\rho$ and the named $\lambda$.$(\lambda _{x}y.f)w$

The following example demonstrates a request. Here the request $\gamma _{x}z.z$ gets the value w from $(\lambda _{x}y.f)w$.

$(\lambda f.(\lambda w.(\lambda _{x}y.f)\ w)\lambda x.x)\ \gamma _{x}z.z$ - beta reduce

$(\lambda w.(\lambda _{x}y.\gamma _{x}z.z)\ w)\ \lambda x.x$

$(\lambda w.(\lambda _{x}y.z[z:=y])\ w)\ \lambda x.x$

$(\lambda w.(\lambda _{x}y.y)\ w)\ \lambda x.x$

$(\lambda w.w)\ \lambda x.x$

$\lambda x.x$

Notes.

• Reduction all ways reduce to a single value. Proof?
• However the same lamda term can represent different values.

Branching clocks

A branching clock allows 2 clocks to be obtained from a clock. The two clocks are called next and branch.

When the time is required in a function call, a clock is branched off while the main sequence of clocks is linked up to the next function.

Stability of the branching clock

In the mathematical model every call to a function with the same parameters must return the same value. So,

$c.{\text{next}}.{\text{branch}}.{\text{next}}.{\text{time}}$

must always return the same result. To achieve this each path in the tree is identified by a bit string, with 0 for next and 1 for branch. When a time is given the time is recorded in a table against the path. When a time is requested again the time recorded against the path is given.

The time table can then be recorded to allow the re-running of the program with the same clock. This allows the reproduction of the exact functionality, which is useful for testing and debugging.

State and imperative programming

On the surface imperative programs are very different from functional programs. However monads provide a way of introducing imperative commands into a functional language, by hiding the state in the monad object.

But monads do not give a completely natural way of representing imperative programming. They do not provide a general model for translating an imperative program into a functional language.

Transformations on imperative programs

Mathematical expressions may be transformed using mathematical rules to give equivalent expressions. The same ability is needed for imperative programs. A mathematical model for an imperative program allows a change in the execution order of the program, without changing the overall effect of the program.

The goal is to integrate imperative statements into mathematics, so that an imperative program may be represented with minimal translation as mathematics.

A function definition in an imperative language is translated into a function definition in mathematics. A program is represented by a conjunction of function definitions.

The mathematics may then be transformed in various ways, using rules that guarantee no change in the meaning of the program.

State holder

Using the relational evaluation model, a simple model of state transfer may be given. A statement in an imperative program has,

• Input state i
• Input parameters p
• return value x
• Output state o

$f(i,p)=(x,o)$

It is natural in a functional to consider the input state as another parameter. But using the relational evaluation model this is not necessary. the relation model allows the output to be used in determining the input. For example in,

$x\cdot 3=9$

x is determined to be 3, when it is only input to the function.

A state holder is represented by a $\sigma _{s}(i,x,o)$.

• s - state identifier.
• i - input.
• x - value.
• o - output.

$f(p)=\sigma _{s}(i,x,o)$

The state identifier will be used to break up monolith state into into individual state variables. Monolithic state is represented by a single program state including all variables.

Because a state holder takes its input from its output, it does not behave in the same way as other mathematical objects. But with its own set of laws it may be included in a mathematical framework.

The advantage of using a state holder is that state may be transferred through any parameter, providing a full model of imperative programming. The state transfer is completely hidden, and there is a direct translation between imperative programs and state holder programs. State only needs to be transferred where needed.

In comparison monads provide only a linear transfer through primary parameters, but not through every parameter.

A disadvantage is that translating an imperative program to a state holder form is that the type system must be used to determine the rules to apply to state holders. Normal mathematical rules such as the definition of equality and the rule of substitution must be modified for state holders.

State identifiers

The usual approach to modelling imperative programs is to consider them to have a single state. State variables access this state to retrieve the value of the variable in that state. However this approach specifies a single execution order on the program. For example,

$x:=5*x;y:=y+1\equiv y:=y+1;x:=5*x$

Reversal of the execution order does not effect the meaning of the program. This is obvious if x and y are modeled separately as two different state variables, but not obvious if there is a single monolithic state. The monolithic state is modified and accessed in both the statements, therefore the $x:=5*x$ must be executed before $y:=y+1$.

However if x and y are two separate states then $x:=5*x$ and $y:=y+1$ are independent statements that each access there own state variable and the order of execution does not effect the result.

The way in which states interact is defined using the following rules,

$\sigma _{s}(i_{s},\sigma _{s}(i_{t},f\ x,o_{t}),o_{s})=\sigma _{s}(i_{s},f\ x,o_{t})$

$s\neq t\to \sigma _{s}(i_{s},\sigma _{t}(i_{t},f\ x,o_{t}),o_{s})=\sigma _{t}(i_{t},\sigma _{s}(i_{s},f\ x,o_{s}),o_{t})$

State holder rules

The use of state holders depends on the use of type signatures to determine what rules to apply. Different rules apply to expressions of types that are state holders. The rules to apply depend on the signatures of the functions and operators. For simplicity two basic type classifications are made,

• Non state holder - n
• State holder - s

For example the type signature,

$s=s\to s$

indicates that the equality operator takes two state holders as parameters, and returns a state holder.

Equality and function definition

Equality is defined by different rules depending on its type signature.

Signature	Rule
$s=s\to s$	Equality defined by, $\sigma _{s}(i_{s},x,o_{s})=\sigma _{t}(i_{t},y,o_{t})=\sigma _{s}(i_{s},\sigma _{t}(i_{t},x=y,o_{t}),o_{s})$ or where $s=t$ $\sigma _{s}(i,x,m)\ \sigma _{s}(m,y,o)=\sigma _{s}(i,x=y,o)$
$s=n\to s$	$x=\sigma _{s}(i,y,o)\equiv \sigma _{s}(i,x=y,o)$
$n=s\to s$	$\sigma _{s}(i,x,o)=y\equiv \sigma _{s}(i,x=y,o)$
$s=s\to {\text{Boolean}}$ $n=n\to {\text{Boolean}}$	Normal mathematical definition of equality, which implies the substitution rule, $a=b\to f(a)=f(b)$

In imperative languages there will be function definitions which are equivalent to mathematical equality, that returns a Boolean. Calls to the function are replaced with the body of the function with formal parameters replaced by actual parameters.

Substitution of parameters

Substitution of formal for actual parameters is allowed if the types match;

• state holder formal parameter with state holder actual parameter.
• non state holder formal parameter with non state holder actual parameter.

Substitution of lambda expressions follows the same rule. The type of the lambda variable must match the type of the expression being substituted.

In an imperative language, function parameters are state holders. Older languages like C++ do not allow a state holder to be directly used as a parameter. Only a named function pointer may be used for a state holder. More recent languages like Java and Javascript allow anonymous functions, which may be represented as state holders.

Assignment statement

The definition of the assignment statement requires the use of the use–mention distinction. In the following definitions $x$ is the use the mention $x_{m}$.

A C style assignment operator may be defined using monolithic state as.

$x:=y\equiv \sigma _{s}(i,y,i[x_{m}:=y])$

$x:=\sigma _{s}(i,y,o)\equiv \sigma _{s}(i,y,i[x_{m}:=y])$

Using state identifiers, the assignment statement may be defined as,

$x:=y\equiv \sigma _{x_{m}}(i,y,y)$

$x:=\sigma _{s}(i_{s},y,o_{s})\equiv \sigma _{x_{m}}(i,\sigma _{s}(i_{s},y,o_{s}),y)$

Use-mention distinction

The use–mention distinction may be illustrated by the statement,

Jane said "Your hair looks scruffy.".

In this statement I have mentioned what Jane said. I can turn the mention into a use by the statement.

I agree with Jane.

Then this is the same as me saying,

Your hair looks scruffy.

Any expression denotes (is a name for) a value. A statement as a usage and denotes one of the values true or false. A statement as a mention has as its value the statement itself, not yet evaluated.

Meta programming uses the $\eta$ to mark a statement as a mention. $\eta (x)$ is a mention of the variable x. It is a piece of code that has not yet been evaluated. $\eta ^{-1}$ evaluates the meta code to give the use.

$\eta ^{-1}(\eta (x))=x$

Note that a use cannot be turned into a mention, because a use already denotes a value.

For example in the statement,

$z:=z+1$

The definition of this as a state holder is

$z:=z+1\equiv \sigma _{z_{m}}(i,z+1,z+1)$

where $z_{m}$ is a mention of the variable z. So,

$\eta ^{-1}(z_{m})=z$

Then letting $x=z_{m}$

$\eta ^{-1}(x):=\eta ^{-1}(x)+1\equiv \sigma _{x}(i,\eta ^{-1}(x)+1,\eta ^{-1}(x)+1)$

In the following definitions,

• $x$ is a meta variable.
• $\eta ^{-1}(x)$ is the use of the variable denoted by the meta variable x.

A C style assignment operator may be defined using monolithic state as.

$\eta ^{-1}(x):=y\equiv \sigma _{s}(i,y,i[x:=y])$

$\eta ^{-1}(x):=\sigma _{s}(i,y,o)\equiv \sigma _{s}(i,y,i[x:=y])$

Using state identifiers, the assignment statement may be defined as,

$\eta ^{-1}(x):=y\equiv \sigma _{x}(i,y,y)$

$\eta ^{-1}(x):=\sigma _{s}(i_{s},y,o_{s})\equiv \sigma _{x}(i,\sigma _{s}(i_{s},y,o_{s}),y)$

Value lookup

Using a monolithic state, for a state s,

$\sigma _{s}(i,y,o)=\sigma _{s}(i,{\text{subst}}(y,i),{\text{subst}}(o,i))$

where $y[x:=i[x]]$ is the expression y with free occurrences of x replaced by i[x]. Free and bound variables are concepts from lambda calculus. A lambda abstraction binds it's variable. Also a state holder binds it's state identifier.

For a state variable x,

$\sigma _{x}(i,y,o)=\sigma _{x}(i,y[x:=i],o[x:=i])$

where $y[x:=i]$ is the expression y with free occurrences of x replaced by i.

Where there is condition evaluation of parameters (if, and, or) an extra rule is required,

$\sigma _{x}(i,y,o)\ (f\ s)=\sigma _{x}(i,y[x:=i],o[x:=i])\ (f[x:=o[x:=i]]\ s)$

where s may be a state holder. Using Currying this rule can be shown to imply,

$m\ \sigma _{x}(i,y,o)\ (f\ s)=m\ \sigma _{x}(i,y[x:=i],o[x:=i])\ (f[x:=o[x:=i]]\ s)$

for example,

$\sigma _{x}(i,y,o);(f\ s)=\sigma _{x}(i,y[x:=i],o[x:=i]);(f[x:=o[x:=i]]\ s)$

Statement composition

The semicolon ; is used in many languages to separate statements, which are executed sequentially. Here it is regarded as an operator.

$\sigma _{s}(i,a,o);b\equiv \sigma _{s}(i,b,o)$

$\sigma _{s}(i,a,m);\sigma _{s}(m,b,o)\equiv \sigma _{s}(i,b,o)$

$s\neq t\to \sigma _{s}(i_{s},a,o_{s});\sigma _{t}(i_{t},b,o_{t})\equiv \sigma _{s}(i_{s},\sigma _{t}(i_{t},b,o_{t}),o_{s})$

State import rule,

$s;(fx)\equiv (s;f)x$

Rules for the composition of polylithic states,

$\sigma _{s}(i,a,m);\sigma _{s}(m,b,o)\equiv a[s:=i];\sigma _{s}(m,b,o)$

$s\neq t\to \sigma _{s}(i,a,m);\sigma _{t}(n,b,o)\equiv a[s:=i];\sigma _{t}(m,\sigma _{s}(i,a,m);b,o[s:=i])$

Function application

Function application of state holders are defined by the following rules,

$f\ \sigma _{s}(i,x,o)=\sigma _{s}(i,f\ x,o)$

$\sigma _{s}(i,f,o)\ x=\sigma _{s}(i,f\ x,o)$

$\sigma _{s}(i_{s},f,o_{s})\ \sigma _{t}(i_{t},x,o_{t})=\sigma _{s}(i_{s},\sigma _{t}(i_{t},f\ x,o_{t}),o_{s})$

Using the state identifier rules, the last rule implies,

$\sigma _{s}(i,f,m)\ \sigma _{s}(m,x,o)=\sigma _{s}(i,f\ x,o)$

State import rule,

$s\ (fx)\equiv \mu (s)\ (s;f)\ x$

State transfer rule,

$sx\equiv \mu (s)\ (s;x)$

Definition of $\mu$,

$\mu (\sigma _{s}(i,x,o))=\mu (x)[s:=x]$

$\mu (x)=x$

Lambda abstraction

Lambda abstraction of state holders is defined by,

$\lambda y.\sigma _{s}(i,x,o)=\sigma _{s}(i,\lambda y.x,o)$

Conditional evaluation and execution control

Conditional evaluation is a form of function application where some parameters are ignored if the value is not needed. Where the value being omitted is a state holder, the transfer of state through the parameter is omitted in some languages, giving control of the execution path.

In this case these functions are treated differently and the function application rules are not applied.

If statement

An if statement may be regarded as a function, with 3 parameters.

• Condition
• True case
• False case

The condition function may be state-full or stateless. Stateless is defined by,

$(\operatorname {if} \operatorname {true} \operatorname {then} a\operatorname {else} b)=a$

$(\operatorname {if} \operatorname {false} \operatorname {then} a\operatorname {else} b)=b$

where a and b may be state holders, or other types.

State import rule. This rule is implied by the state import rule defined in function application.

$s;{\text{if}}\ c\ {\text{then}}\ a\ {\text{else}}\ b\equiv {\text{if}}\ s;c\ {\text{then}}\ a\ {\text{else}}\ b$

State transfer rule. This rule overrides general state transfer rule in function application.

${\text{if}}\ s\ {\text{then}}\ a\ {\text{else}}\ b\equiv {\text{if}}\ \mu (s)\ {\text{then}}\ (s;a)\ {\text{else}}\ (s;b)$

Statement append rule.

$({\text{if}}\ s\ {\text{then}}\ a\ {\text{else}}\ b);d\equiv {\text{if}}\ s\ {\text{then}}\ (a;d)\ {\text{else}}\ (b;d)$

And expression

In some imperative languages such as C the second condition is only executed if required to compute the result. This is defined by,

$\operatorname {true} \land a=a$

$\operatorname {false} \land a=\operatorname {false}$

$\sigma _{s}(i,c,m)\land a\equiv \sigma _{s}(i,c,m);c\land a$

Or expression

Similarly for an or exression || in C the second condition is only executed if required to compute the result. This is defined by,

$\operatorname {true} \lor a=a$

$\operatorname {false} \lor a=\operatorname {false}$

$\sigma _{s}(i,c,m)\lor a\equiv \sigma _{s}(i,c,m);c\lor a$

Loops

While loops and other control structures may be implemented as functions that take state holders as parameters. The while statement is defined by,

$\operatorname {while} c\operatorname {do} b=\operatorname {if} c\operatorname {then} (b;\operatorname {while} c\operatorname {do} b)$

If b and c are not a state holders this statement either does nothing or expands recursively forever. If b or c are state holders, the value returned by c does not need to be the same each time, even though the expression is the same.

Return values

The natural structure is that the body of the function is an expression. The return value of the function is the value of the expression. The function call is then equal to the body of the function, with formal parameters replaced by actual parameters. The return value may be stateless, or it may be a state holder.

However, many imperative languages like C ignore the value returned from the expression and rely on the return statement to capture a value from a state. An extra structure called the return frame is needed to implement this structure.

Return frame

The return frame accepts the return value. The value may be stateless, or a state holder.

$\operatorname {returnframe} (s;\operatorname {return} )\equiv s$

provided s does not contain any return statements.

Return statement

The return statement is defined by,

$\operatorname {return} x\equiv x;\operatorname {return}$

$\operatorname {return} ;{\text{destroy}}\ x\equiv {\text{destroy}}\ x;\operatorname {return}$

The return statement does not execute statements after the return, other than destroy.

$\operatorname {return} ;u=\operatorname {return}$

if u is a single statement, other than a destroy statement.

Examples

Factorial function

The factorial function may be defined using a while loop by,

long fact(long n)
{
  long r = 1;
  while (0 < n)
  {
    r = r * n;
    n = n - 1;
  }
  return r;
}

A direct translation of this imperative code to relational logic using state holders is,

${\text{fact}}\ n_{p}={\text{returnframe}}({\text{var}}\ n:({\text{var}}\ r:(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r*n;n:=n-1);{\text{return}}\ r)))$

Remove return frame

${\text{fact}}\ n_{p}={\text{returnframe}}({\text{var}}\ n:({\text{var}}\ r:(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r*n;n:=n-1);{\text{return}}\ r)))$

• ${\text{var}}x:(s)\equiv s;{\text{destroy}}\ x$ .......... See local state variables

${\text{fact}}\ n_{p}={\text{returnframe}}(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r*n;n:=n-1);{\text{return}}\ r;{\text{destroy}}\ r;{\text{destroy}}\ n)$

• ${\text{return}}\ r\equiv r;{\text{return}}$ .......... See return frame

${\text{fact}}\ n_{p}={\text{returnframe}}(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r*n;n:=n-1);r;{\text{return}};{\text{destroy}}\ r;{\text{destroy}}\ n)$

• ${\text{return}};{\text{destroy}}\equiv {\text{destroy}};{\text{return}}$ .......... See return frame

${\text{fact}}\ n_{p}={\text{returnframe}}(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r*n;n:=n-1);r;{\text{destroy}}\ r;{\text{destroy}}\ n;{\text{return}})$

• $\operatorname {returnframe} (s;\operatorname {return} )\equiv s$ .......... See return frame

${\text{fact}}\ n=(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r\cdot n;n:=n-1);r;{\text{destroy}}\ r;{\text{destroy}}\ n)$

Remove assignment statements

${\text{fact}}\ n=(n:=n_{p};r:=1;{\text{while}}\ 0<n\ {\text{do}}\ (r:=r\cdot n;n:=n-1);r;{\text{destroy}}\ r;{\text{destroy}}\ n)$

• $x:=y\equiv \sigma _{x_{m}}(i,y,y)$ .......... See assignment statement

${\text{fact}}\ n=\sigma _{n}(i_{1},n_{p},n_{p});\sigma _{r_{m}}(i_{2},1,1);{\text{while}}\ 0<n\ {\text{do}}\ (\sigma _{r_{m}}(i_{r},r\cdot n,r\cdot n);\sigma _{n_{m}}(n_{i},n-1,n-1));r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• $s\neq t\to \sigma _{s}(i_{s},a,o_{s});\sigma _{t}(i_{t},b,o_{t})\equiv \sigma _{s}(i_{s},\sigma _{t}(i_{t},b,o_{t}),o_{s})$ .......... See statement composition

${\text{fact}}\ n=\sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n$

Expand while loop

${\text{fact}}\ n=\sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• $\operatorname {while} c\operatorname {do} b=\operatorname {if} c\operatorname {then} (b;\operatorname {while} c\operatorname {do} b)$ .......... See loops.

${\text{fact}}\ n=\sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n));r;{\text{destroy}}\ r;{\text{destroy}}\ n$

Simplify if statement

${\text{fact}}\ n=\sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n));r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• $s;{\text{if}}\ c\ {\text{then}}\ a\ {\text{else}}\ b\equiv \mu (s){\text{if}}\ s;c\ {\text{then}}\ a\ {\text{else}}\ b$ .......... See if statement

${\text{fact}}\ n={\text{if}}\ \sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});0<n\ {\text{then}}\ (\sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n));r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• ${\text{if}}\ s\ {\text{then}}\ a\ {\text{else}}\ b\equiv {\text{if}}\ \mu (s)\ {\text{then}}\ (s;a)\ {\text{else}}\ (s;b)$ .......... See if statement

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});\sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n))\ {\text{else}}\ \sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• $\sigma _{s}(i,a,m);\sigma _{s}(m,b,o)\equiv \sigma _{s}(i,b,o)$ .......... See statement composition ????

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{p},n-1,n-1),n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{p},n-1,n-1),r\cdot n))\ {\text{else}}\ \sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• $({\text{if}}\ s\ {\text{then}}\ a\ {\text{else}}\ b);d\equiv {\text{if}}\ s\ {\text{then}}\ (a;d)\ {\text{else}}\ (b;d)$ .......... See if statement

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{p},n-1,n-1),n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n)\ {\text{else}}\ \sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});r;{\text{destroy}}\ r;{\text{destroy}}\ n$

• $\sigma _{s}(i,a,o);b\equiv \sigma _{s}(i,b,o)$ .......... See statement composition

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{p},n-1,n-1),n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{p},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n)\ {\text{else}}\ \sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{destroy}}\ r;{\text{destroy}}\ n$

Destroy values

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{i},n-1,n-1),n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n)\ {\text{else}}\ \sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{destroy}}\ r;{\text{destroy}}\ n$

• $\sigma _{x}(i,y,o);{\text{destroy}}\ x\equiv y$ ......... See local state variables

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ (\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{i},n-1,n-1),n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n)\ {\text{else}}\ 1$

Consider the sub expression,

$(\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{i},n-1,n-1),n);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n)$

The initial value for r is $n_{p}$ which is a multiplied by other factors to get the result. So if this value is divided by $n_{p}$ and the whole expression is multiplied by $n_{p}$, the result will be the same,

$=n_{p}\cdot (\sigma _{r_{m}}(1,\sigma _{n_{m}}(n_{i},n_{p}-1,n_{p}-1),1);{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n)$

Earlier at the end of removing assignment statements, ${\text{fact}}\ n=\sigma _{n}(i_{1},\sigma _{r_{m}}(i_{2},1,1),n_{p});{\text{while}}\ 0<n\ {\text{do}}\ \sigma _{r_{m}}(i_{r},\sigma _{n_{m}}(n_{i},n-1,n-1),r\cdot n);r;{\text{destroy}}\ r;{\text{destroy}}\ n$

so the sub-expression is equal to,

$=n_{p}\cdot {\text{fact}}\ (n-1)$

and,

${\text{fact}}\ n={\text{if}}\ 0<n\ {\text{then}}\ n\cdot {\text{fact}}\ (n-1)\ {\text{else}}\ 1$

Comparison to other representations

The state holder may be applied to function application where the parameters are state holders. Other approaches such as monads implement state under composition of statements, but not application. This limits there ability to fully represent imperative programs, and the ability to integrate imperative programming into mathematics.

References

Category:Computer science