Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
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
|
|
|
|
