Symbolic Logic:Programming:Function to Fact Transformation

From Knowino

(Redirected from Function to Fact Transformation)

Pending changes are displayed on this page

Unchecked

Jump to: navigation, search

Functions treat the return value (result) differently from the parameters. The result is calculated from the parameters. There is no explicit variable into which the value will be entered.

In Demand Driven Evaluation we will show how the requested variable can be calculated from the other parameters (including the result). This makes the role return value equivalent to the parameters. As the return value is not necessary the value that is calculated, from a structural point of view it behaves in the same way as a parameter.

But the imperative programming languages that we will be building on do treat the return value differently from the parameters. There is no variable to contain the return value.

So to make this clear and precise we need a transformation of a function, that turns the return value into an extra parameter.

[edit] Function Transformations

A call to a function looks like,

$f(x, y, z, ...) \!$

That is a function $f \!$ is applied to some parameters $x, y, z, ... \!$ . Other forms of the function are needed in order to transform functions into the form required for Demand Driven Evaluation. The List Equivalent Function $L(f)\!$ is,

$L(f)([x, y, z]) = f(x, y, z) \!$

the inverse of this function is $L^{-1}(f)\!$ .

D1 $L^{-1}(L(f)) = f \!$

so,

$g([x, y, z]) = L^{-1}(g)(x, y, z) \!$

The List Equivalent Function may be defined using Curried functions,

D2 $L(f)(x|y) = f_{curry}(x)(y) \!$

or,

D2 $f(x|y) = L^{-1}(f)_{curry}(x)(y) \!$

Lists are manipulated using,

List prepend,

$x|[a, b, c] = [x, a, b, c] \!$

List concatenation

$[a, b, c]+[x, y] = [a, b, c, x, y] \!$

Demand Driven Evaluation requires the result to be treated in the same way as paramaters. The Result Equivalent Function $R(f)\!$ is defined,

D3 $R(f)(x+[r]) \iff f(x) = r \!$

The goal is to transform expressions to equivalent forms as Result Equivalent Functions. For example to transform an expression.

$x = y^2 + 5 \!$

The use of operators is syntactic sugar. Each of the operators could be replaced with functions,

$equals(x, plus(power(y, 2), 5) \!$

and this function can be transformed into,

$L(equals)([x, L(plus)([L(power)([y, 2]), 5])]) \!$

The goal is to transform this expression into,

$R(L((equals))([x, b, result]) \and R(L((plus))([c, 5, b]) \and R(L((power))([y, 2, c]) \!$

This is the Result Equivalent Transformation (RET). This transformation is the subject of the next section.

For simplicity define $LRL(xf) = L^{-1}(R(L(f)))\!$ .

$LRL(equals)(x, b, result) \and LRL(plus)(c, 5, b) \and LRL(power)(y, 2, c) \!$

[edit] The Result Equivalent Transformation (RET)

Starting with a function call,

$g(x, y, z ...) \!$

The List Equivalent Expression is,

$f(c) \!$

where,

$f = L(g) \!$

$c = [x, y, z ...] \!$

Using D3,

$f(c) = R(f)(c+[true])\!$

Both $f \!$ and $c \!$ could be either constants, variables, or calls to functions. If they are calls to functions they must be replaced by variables.

Let,

$f = k(m)\!$

$g = l(n)\!$

$R(x)(y+[true]) \and k(m)=x \and l(n)=y \!$

or

$R(x)(y+[true]) \and R(k)(m+[x]) \and R(l)(n+[y]) \!$

and now a recursive pattern appears.

[edit] The RET Tuple

A data representing the state of process is recorded in the RET Tuple (RETT).

The RET Tuple has attributes,

An expression
- On input, the input expresion being processed.
- On output the variable containing the result variable, or a constant or other variable.
A RET expression $s \!$ .

The definition,

$\forall y\in RETT: y = (y_c, y_s)\!$

allows access to the components of an RETT.

The RET function takes an RETT as a parameter and returns a RETT as a result.

[edit] Rule 1

$RET((f(c), s)) = (x, y_s \and R(z_c)(y_c+[x])) \!$

$\and y = RET((c, z_s)) \!$

$\and z = RET((f, s)) \!$

[edit] Rule 2

$\! RET( (a|b, s) ) = (z_c|y_c, y_s) \!$

$\and y = RET((b, z_s)) \!$

$\and z = RET((a, s)) \!$

[edit] Rule 3

To be applied only if rule 1 cant be applied.

$RET((x, s)) = (x, s) \!$

[edit] Simplified rule 1

If f is a constant or variable rule 1 simplifies down to,

$RET((f(c), s)) = (x, y_s \and R(f)(y_c+[x])) \!$

$\and y = RET((c, s)) \!$

[edit] Example

The example in Function Transformations is,

$L(equals)([x, L(plus)([L(power)([y, 2]), 5])]), \!$

For readability define $L(f) = f_l \!$ . Applying the RET function is,

$RET(equals_l([x, plus_l([power_l([y, 2]), 5])]), true) \!$

[edit] Step 1

Applying the simplified rule 1.

$(x, j_s \and R(equals_l)(j_c+[x])) \!$

where, $j = RET(([x, plus_l([power_l([y, 2]), 5])], true)) \!$

Applying rule 2 a couple of time and rule 3 once gives,

$(result, k_s \and R(equals_l)([x, k_c, result])) \!$

where, $k = RET((plus_l([power_l([y, 2]), 5]), true)) \!$

[edit] Step 2

To expand $RET((plus_l([power_l([y, 2]), 5]), true)) \!$ apply the same process,

$(result, k_s \and R(equals_l)([x, k_c, result])) \!$

where, $k = (a, m_s \and R(plus_l)([m_c, 5, a])) \!$

and, $m = RET((power_l([y, 2]), true)) \!$

or,

$(result, m_s \and R(plus_l)([m_c, 5, a]) \and R(equals_l)([x, a, result])) \!$

where, $m = RET((power_l([y, 2]), true)) \!$

[edit] Step 3

To expand $RET((power_l([y, 2]), true)) \!$ apply the process again,

$(result, m_s \and R(plus_l)([m_c, 5, a]) \and R(equals_l)([x, a, result])) \!$

where, $m = (b, true \and R(power_l)([y, 2, b])) \!$

or,

$(result, R(power_l)([y, 2, b]) \and R(plus_l)([b, 5, a]) \and R(equals_l)([x, a, result])) \!$

This gives the Return Equivalent transformation of,

$equals_l([x, plus_l([power_l([y, 2]), 5])])\!$

as,

$R(power_l)([y, 2, b]) \and R(plus_l)([b, 5, a]) \and R(equals_l)([x, a, result]) \!$

with the returned value of $result \!$

[edit] Meta Mathematics

The RET function is described above as if it is a function when really it should be a meta function. The distinction is quite subtle.

The RET function is intended to a mathematical expression, and rearrange it to form another mathematical expression. But that is not quite what I have described. All I have done is write some new theorems that are implied by,

D3 $R(f)(x+[r]) \iff f(x) = r \!$

To fix this problem I need,

A way of representing a mathematical expression as something to be worked on.
Some types (or sets) to which expressions can belong.

[edit] Mathematics as Data

The mathematics about mathematics idea is what has been come to be though of by meta mathematics. I wanted a short symbol to represent meta so I chose the greek letter $\eta \!$ (eta). It is short and it rhymes with meta.

Writing mathematics as data is the inverse of writing mathematics about mathematics. So this is $\eta^{-1} \!$ . This demotion of mathematics allows meta mathematics to be written. For example

$\eta^{-1}[ x^2 + 1 = 0 ]) ] \!$

is an expression representing some mathematics, not the mathematics,

The difference can be seen in the types,

$(x^2 + 1 = 0) \in bool \!$

whereas,

$\eta^{-1}[ x^2 + 1 = 0 ] \in expression \!$

The square brackets are used to indicate that $\eta^{-1} \!$ is not a function. It is a change of the meaning of the text between the square brackets.

$\eta \!$ is used to put variables into meta mathematics. For example, if,

$f = \eta^{-1}[sin] \!$

$x = \eta^{-1}[\pi / 4] \!$

then

$\eta^{-1}[\eta[f](\eta[x]) ] = \eta^{-1}[sin(\pi / 4) ] \!$

[edit] Types for Meta Mathematics

Type	Description	Example
expression	any mathematical expression	$x 2 * 5$
call	a call to a function	$f a c t o r i a l (5)$
variable	a variable (placeholder for a value)	$x$
constant	a constant value	$5, e,π, f a c t o r i a l$ as in the function name.
construction	a set or list construction	$[5,6,7],{0,1}$