User:Thepigdog/Play

Impossible to convert a program without meta logic.

$fp=\lambda i.(r,o)$

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

$\lambda i.(f,m)\ (\lambda m.(x,o)\ m)=\lambda i.(f\ x,o)$

$\alpha i\eta (fp)=(r(\alpha ieta(f)))(\alpha (o(\alpha ieta(f)))eta(p))$

$\alpha ifp=(r(\alpha if))(\alpha (o(\alpha if))p)$

$hf(p)g(q)=h(\lambda i.(r_{p},o_{p}))(\lambda i.(r_{q},o_{q}))$

$hf(p)g(q)=h(\lambda i.(r_{p},o_{p}))(\lambda i.(r_{q},o_{q}))o_{p}$

$fp=f(po(f))$

$\alpha f;p=pf$

$\alpha ifp=(r(\alpha if))(\alpha (o(fi))p)$

$r(\alpha if)=i[f]$

$o(\alpha if)=f$

$\alpha i(x:=v)=({\text{true}},i[x:=v])$

$i[x:=v]x=v$

$\alpha i(x:=v)=({\text{true}},i[\eta (x):=v])$

$i[x:=v]x=v$

Junk

Imperative programs allow the modification of state. State consists of many state variables. A state variable is the name which identifies different values at different points in the execution of a program.

For each state variable, a statement has an input value and an output value. The input value and the output value may be the same, or the statement may calculate a new output value from the input value.

To represent this mathematically, a statement has an input i, parameters p, and output r, and an output o. An imperative statement,

$f(p)=r$

actually means,

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

The return value and the output state are calculated from the input state and the parameter. In a series of statements the outputs of proceeding statements need to be connected to the inputs of proceeding statements. An imperative statement does not explicitly represent this input.

The input state is not explicitly represented. One possibility is that the function should be represented as a lambda expression

$f(p)=\lambda i.(r,o)$

State passed by function composition

In many languages the ; is used to separate statements. For example.

$x:=6;x=x+1;x:=x*2$

An assignment statement is represented as a lambda expression as,

$a:=b\equiv \lambda i.i[\eta (a):=b]$

If the statement separator is regarded as function composition,

$r;s\equiv r\circ s=s\ r$

Then the series of statements becomes,

$x:=6;x:=x+1;x:=x*2$

$\equiv ((\lambda i.i[\eta (x):=6]\circ \lambda i.i[\eta (x):=i[x]+1])\circ \lambda i.i[\eta (x):=i[x]*2])$

$\equiv (\lambda i.i[\eta (x):=i[x]*2])\ (\lambda i.i[\eta (x):=i[x]+1])\ (\lambda i.i[\eta (x):=6])\ s$

$\equiv (\lambda i.i[\eta (x):=i[x]*2])\ (\lambda i.i[\eta (x):=i[x]+1])\ s[\eta (x):=6]$

$\equiv (\lambda i.i[\eta (x):=i[x]*2])\ s[\eta (x):=6][\eta (x):=s[\eta (x):=6][x]+1]$

$\equiv (\lambda i.i[\eta (x):=i[x]*2])\ s[\eta (x):=6][\eta (x):=7]$

$\equiv (\lambda i.i[\eta (x):=i[x]*2])\ s[\eta (x):=7]$

$\equiv s[\eta (x):=7][\eta (x):=s[\eta (x):=7][x]*2]$

$\equiv s[\eta (x):=7][\eta (x):=14]$

$\equiv s[\eta (x):=14]$

Another approach is to regard the assignment statement as a lambda expression,

$a:=b;c\equiv (\lambda a.c)\ b$

$a:=b\equiv b$

Then by use of bracketing,

$x:=6;(x:=x+1;x:=x*2)$

$\equiv (\lambda x.x:=x+1;x:=x*2)\ 6$

$\equiv (\lambda x.(\lambda x.x:=x*2)\ x+1)\ 6$

$\equiv (\lambda x.(\lambda x.x*2)\ 6)x+1)$

$\equiv 14$

However both these approach only work for a series of statements. For imperative functions with side effects returning results that are combined using other operators this approach does not give the right structure.

State under function application

In the relational programming model it is not necessary to consider the output as being calculated from the input. The state holder notation includes the input as part of a triple returned by the function.

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

In this representation the state holder does not actually behave like a mathematical object. It does not obey the substitution rule,

$a=b\implies g(a)=g(b)$

But is a good fit for an assignment statement, which is also not mathematical.

For example,

$x:=5;x:=x+1$

The assignment statement here is interpreted as returning the value true if it is successful. Note that this is not the interpretation in the C language, but it allows the ; to be interpreted as conjunction,

$x:=5\land x:=x+1$

Using state holders this expression is equivalent to,

$\sigma _{x}(x_{1},{\text{true}},5)\land \sigma _{x}(x_{2},{\text{true}},x_{2}+1)$

As the output of the first statement is the input to the next statement then,

$x_{2}=5$

and the statement simplifies to,

$\sigma _{x}(x_{1},{\text{true}},6)$

which is equivalent to,

$x:=6$

The triple of input, result, and output is called a state holder.