Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Topic: Program Construction (Synthesis) is (virtually) Programming Language Independent
Replies: 0

 Charlie-Boo Posts: 1,600 Registered: 2/27/06
Program Construction (Synthesis) is (virtually) Programming Language Independent
Posted: Feb 11, 2013 12:08 PM

I have taken my Program Synthesis to a very low level ? a formal
system for manipulating programs (rather than a set of hard-wired
functions for your programming language) and discovered something
truly amazing.

First recall that all research into program analysis (Hoare) and
program synthesis (Manna/Waldinger, Martin-Löf) has been to examine
the individual commands and other programming language constructs, and
build programs from them. Just like a programmer does.

But the truth is, none of the details of a program are relevant to
using it in the construction of other programs, other than breaking it
into 3 segments: the code before output command ECHO, the ECHO, and
the code after the ECHO. (This is applied to each ECHO.)

This shows that current research examining individual commands is ALL
A WASTE, while the fact that they have zero examples of actual formal
program constructions ? formal details not vague descriptions ? shows
the result. (All BS references explained for 1 Euro each.)

DETAILS

I showed on ARXIV how to build programs from programs, using 8 Rules
of Inference (NOT, AND, OR, QUIT, DO, IF, UNION, SUB.) The programs
were combined by unspecified programs that were assumed to exist e.g.
map a program that decides a set to one that decides its complement by
changing output x to output not(x) for some program code for output
and not.

Now I have generalized these functions and the result is there are 4
programming language constructs needed to carry out the program
construction, and:

The details of how to form the new program are independent of the
Programming Language!!

The 4 constructs:

ECHO to output the value of a given expression.
IF and ELSE to conditionalize execution.
Value 0 for false and value 1 for true.
\$v= save a value into a newly introduced variable.

Let [1] etc be an arbitrary sequence of code.
P is any set.
P(I) means to decide P (output whether a given input is an element of
P.)
P(x) means to enumerate P (list its elements.)
SPEC = P(I) or P(x)
PROGRAM #SPEC = program calculates (decides or enumerates)
specification.
=> = Implication

NOT Rule:

[1] echo A [2] # P(I) => [1] { if (A) { echo 0 ; } else { echo
1 ; } ; } ; [2] # ~P(I)

Example:
I<J: ?echo \$i<\$j ;?
I~<J: ?{ if (\$i<\$j) { echo 0 ; } else { echo 1 ; } ; } ;?

Let P1 = [1] echo A [2]
Let P2 = [1] { if (A) { echo 0 ; } else { echo 1 ; } ; } ; [2]

If P1 # P(I) then P2 # ~P(I)

If program P1 decides set P then program P2 decides set ~P.

Given program P1 to decide P we can construct P2 to decide ~P. This
is the simplest of the 8 Rules of Inference for program construction
(program synthesis.)

I developed it for PHP but it looks like it applies to C++, JAVA etc.
but I haven?t check.

Does it apply to all Programming Languages?

The other 7 rules decide the conjunction and disjunction of 2 sets
given a decider for each (AND, OR), the subset of an enumerated set
accepted by a decider of another set (DO), enumerate the union of 2
enumerated sets (UNION), list a set if a decider passes and list the
empty set otherwise (IF), decide if an enumerated set is not empty
(QUIT), and substitute a literal or enumerated set values for the
input to a decider or enumerator (SUB.)

Example:

Rule AND decides the intersection of two decided sets.

[1] echo A [2] # P(I)
[3] echo B [4] # Q(I)
= >
[1] { if (A) { [3] echo B [4] } else { echo A } ; } ; [2]

Or:

[1] { if (A) { P2 } else { echo A } ; } ; [2]

When P1 (top line) is about to echo whether or not the input is in P,
instead it checks if the input is in Q if it is in P, otherwise it
outputs the first check which must be FALSE. Note that 0 and 1 are
used in NOT, but not in AND and OR!

And UNION requires no constructs!

ATTN Manna & Waldinger: Proof by Induction does NOT create a loop!
The existential quantifier does!!

Also note that PROGRAM SYNTHESIS => THEORY OF COMPUTATION =>
INCOMPLETENESS IN LOGIC (for the latter see 18 Word Proof in FOM July
2010.)

C-B