Symbolic Logic:Programming:Language Transformations

Unchecked

There are a number of standard language transformations that allow languages to be converted to other languages.

• Abstract Syntax Tree Transformation
• Scope Transformation
• Non standard feature transformations
• Role transformation

These transformations explain the relationship between languages.

[edit] Abstract Syntax Tree Transformation

The syntax for a language describes the set of strings that are structurally legal in a language. In BNF the syntax for a simple expression may be written as:

<expression> ::= <term> "+" <expression> | <expression> "=" <term>
<term>       ::= <factor> "*" <term> | <factor>
<factor>     ::= <number> | <variable> | "(" <expression>

with appropriate definitions for the number and name functions. The equivalent desciption in mathematical logic is,

"+"

"*"

"("")"

When you call expression() the resulting value is the value set of of all expressions in this simple language. For example you could write,

"x + y * (5 + 6)"

which would evaluate to true.

But this tells you nothing about the syntactic structure of the language. The syntactic structure identifies what part of the string has what role to play. An Abstract Syntax Tree gives this extra information. For this we need classes representing the nodes in the Abstract Syntax Tree.

class Expression1 : Expression
{
private:
    Term term;
    Expression expression;
public:
    string t()
    {
        term.t() + "+" + expression.t();
    }

class term1 : Term
{
private:
    Factor factor;
    Term term;
public:
    string t()
    {
        factor.t() + "*" + term.t();
    }
}

class Factor1 : Factor
{
private:
    Number number;
public:
    string t()
    {
        numbet.t();
    }
}

class Expression2 : Expression
{
private:
    Term term;
public:
    string t()
    {
        term.t();
    }
}

class Term2 : Term
{
private:
    Factor factor;
public:
    string t()
    {
        factor.t();
    }
}

class Factor2 : Factor
{
private:
    Name name;
public:
    string t()
    {
        name.t();
    }
}

class Factor3 : Factor
{
private:
    Expresssion expression;
public:
    string t()
    {
        "(" + expression.t() + ")"
    }
}

[edit] Scope Transformation

For example,

namespace X
{
    void swap(long x, long y)
    {
        long t = x;
        x = y;
        y = t;
    }
}
 
void main()
{
    long x = 5;
    long y = 6;
    x = x + 1;
    X::swap(x, y);
    printf("%ld, %ld", x, y);
}

void X_swap(long X_swap_x, long X_swap_y)
{
    long X_swap_t = X_swap::x;
    X_swap_x = X_swap_y;
    X_swap_y = X_swap_t;
}
 
void main()
{
    long x = 5;
    long y = 6;
    x = x + 1;
    X_swap(x, y);
    printf("%ld, %ld", x, y);
}

void swap( long X_swap_x_1    // input role for x
         , long &X_swap_x2    // output role for x
         , long X_swap_y_1    // input role for y
         , long &X_swap_y_2   // output role for y)
{
    long X_swap_t_1 = X_swap_x_1;
    X_swap_x_2 = X_swap_y_1;
    X_swap_y_2 = X_swap_t_1;
}
 
void main()
{
    long x_1 = 5;
    long y_1 = 6;
    x_2 = x_1 + 1;
    X_swap(x_2, x_3, y_1, y_2);
    printf("%ld, %ld", x_3, y_2);
}

In logic,

Simplifies to,

so,

    printf("%ld, %ld", x_3, y_2);

becomes,

    printf("%ld, %ld", 8, 6);

[edit] Scope Rules

By considering only the details of the language relevant to the scope transformation, the description can be made simpler and more general. A program in a language is simplified down as to be,

• an element
  • which has a vector of sub elements.

An elemented is represented as where v is the vector of sub elements.

The scope transsformation uses the parameters,

• T - The symbol table - associates names with declarations.
• N - The name list - a list of names describing the current naming scope/namespace.

The rules for traversing the program are defined by the scope function,

Any of the scope statements,

 {
      ...
 }

 {
      ...
 }

 {
      ...
 }

adds MyScope/MyClass/MyFunction to the name list describing the current scope.

A statement that adds to the scope is represented as,

The rule for a scope statement is,

A class or function declaration that adds to the scope and declares a name is represented as,

where

• n - The name to be declared and added to the scope.
• s - The signature identifying the object being declared.
• o - The description of the object being declared.
• v - A list of language sub elements.

The rule for a declaration statement is,

[edit] Non standard feature transformations

There are some language features that are not naturally consistent with logic,

• return
• continue
• break
• pointers (other than simple pointers that may be treated as references)

[edit] Role transformations

A role is the name for a variable that acts, in the role, at that point in the program.

In an imperative language a "variable" does not identifier a single value (or value set). The same "variable" identifies different values at different points in the program.

In fact, a "variable" in an imperative programming language is not a variable, it is a role. A role may have an input variable and an output variable. The output variable becomes the input variable for a role in the next statement in the program.

A role transformation converts a program written using roles into a program using variables. In an imperative program all "variables" (other than member variables) are in fact roles. A role transformation converts an imperative program into a logical/functional program.

A logical/functional program is a program that, after Scope Transformation, has for each variable a single set of values (a value set) for every occurrence of the variable.

A role is a name that represents different variables at different points in the program. In each function call a role actual parameter (for a reference formal parameter) represents two variables; an input variable and an output variable. The output variable for a role is the input variable for the next occurrence of the role.

A simple example demonstrates the transformation,

    void f(X &x);
 
    f(y);
    f(y);

    void f(X x1, X &x2);
 
    f(y1, y2);
    f(y2, y3);

[edit] Example

namespace X
{
    void swap(long x, long y)
    {
        long t = x;
        x = y;
        y = t;
    }
}
 
void main()
{
    long x = 5;
    long y = 6;
    x = x + 1;
    X::swap(x, y);
    printf("%ld, %ld", x, y);
}

void X.swap(long &x, long &y)
{
    long t = x;
    x = y;
    y = t;
}
 
void main()
{
    long x = 5;
    long y = 6;
    x = x + 1;
    X.swap(x, y);
    printf("%ld, %ld", x, y);
}

void X.swap( long x_1      // input role for x
           , long &x_2    // output role for x
           , long y_1     // input role for y
           , long &y_2    // output role for y)
{
    long t_1 = x_1;
    x_2 = y_1;
    y_2 = t_1;
}
 
void main()
{
    long x_1 = 5;
    long y_1 = 6;
    x_2 = x_1 + 1;
    X.swap(x_2, x_3, y_1, y_2);
    printf("%ld, %ld", x_3, y_2);
}

In logic,

Simplifies to,

so,

    printf("%ld, %ld", x_3, y_2);

becomes,

    printf("%ld, %ld", 8, 6);

[edit] State

The state maps roles to variables. It is a set of tuples. The expression is a new state with a new unique variable name assigned to r. Mathematically,

is a new unique variable, constructed from v. For example there may be a series of names,

gives the variable associated with a role in a state .

[edit] Role

By considering only the details of the language relevant to the role transformation, the description can be made simpler and more general. A program in a language is simplified down as to be,

• an element
  • which has a vector of sub elements.

An elemented is represented as where v is the vector of sub elements. The rules for traversing the program are defined by the role function,

As you can see the order of the elements is the order used by the role transformation.

An actual parameter for a reference parameter is writen,

The rule for a reference parameter is,

If the element is none of the above the exception condition applies,

where,

[edit] Functions and Formal Parameters

An element can be a function declaration,

where is the function name, is the list of parameters, and is the body.

The role transformation for a function declaration is,

The rules for transforming parameters are,

A role formal parameter that is a reference parameter is written,

A formal parameter is defined by,

The default rule is,

[edit] Member Variables

Member transform differently to other variables in a role transfornations.

!!! to be completed !!!

[edit] Example

[edit] Equivalent Features

The following table shows the correspondence between imperative language C++ and logic. This is a fairly informal description. A more accurate description, would be that, after applying the transformations described above these features are equivalent. This table is intended as a guide.

Id	Description	C++	Description	Logic
1	boolean function	bool f(P p) {return g(p);}	f(p) implies g(p)
2	method	void f(P p) {g(p);}	f(p) implies g(p)
3	function	T f(P p) {return g(p);}	t = f(p) implies t = g(p)
4	function	T f(P p) {h(p); return g(p);}	t = f(p) implies h(p) and t = g(p)
5	result = x	return x
6	statements	A; B	A and B
7	assignment	a = b;	the output role a = the input role b
8	reference parameter	f(T &t)	input role + output role

[edit] Links

• Symbolic Logic:Programming:Change In Time
• Symbolic Logic:Programming:Logic Application
• Symbolic Logic:Programming
• Intelligence and Reasoning