Name
Abstract | ||
|---|---|---|
Various theories have been discussed to formalize computation and to develop new methods of programming. The theory EON+-mu which has the facility of defining predicates recursively is presented. The theory EON+-mu is constructed by adding the facility of recursive definition of predicates to Beeson's EON. Recursively defined data such as lists and trees can be introduced naturally using recursively defined predicates. This facility also enables us to represent a specification formula of a program more easily. In Hayashi's PX, the facility of recursive definition of predicates, called conditional inductive generation, can be used under the syntactical condition that recursive calls of the original predicate occur only in Harrop subformulae. In this paper, a less restricted class of recursively defined predicates can be used. Not only a predicate whose recursive calls occur in Harrop subformulae but a predicate whose recursive calls occur at strictly positive positions is available. This class includes the class of inductive definition with Horn clauses used in Prolog, because of our weaker restriction of strictly positive occurrences of recursive calls. The extended q-realizability interpretation of EON+-mu in EON+-mu is given to treat the recursive definition of predicates. A recursively defined predicate is interpreted as another recursively defined predicate naturally corresponding to the original predicate by this q-realizability interpretation. The soundness of the interpretation is proved in favor of the syntactical condition of recursively defined predicates. A method of program synthesis using q-realizability interpretation in this theory is presented. This method of program synthesis is explained by several examples. |
Year | DOI | Venue |
|---|---|---|
1991 | 10.1016/0304-3975(91)90002-J | Theor. Comput. Sci. |
Keywords | DocType | Volume |
Program synthesis | Journal | 90 |
Issue | ISSN | Citations |
2 | 0304-3975 | 8 |
PageRank | References | Authors |
1.73 | 1 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Makoto Tatsuta | 1 | 111 | 22.36 |