scholarly journals Design of Nondeterministic Program Termination Based on the Equivalent Transformation Computation Model

2006 ◽  
Vol 10 (3) ◽  
pp. 349-361
Author(s):  
Itaru Takarajima ◽  
◽  
Kiyoshi Akama ◽  
Ikumi Imani ◽  
Hiroshi Mabuchi ◽  
...  
Keyword(s):  
Programming Languages ◽  
Program Synthesis ◽  
Equivalent Transformation ◽  
Sufficient Condition ◽  
Model Computation ◽  
Computation Model ◽  
Program Termination ◽  
Nondeterministic Program

We studied the termination of nondeterministic programs, which play an important, basic role in program synthesis, and provide a foundation for proving program termination. The class of programs we consider here is based on the <I>equivalent transformation (ET)</I> computation model. Computation with this model involves the succesive application of rules to sets of clauses. Since the ET model has more expressive terms and rules than other programming languages, program termination is difficult to prove: we must take into account all possible changes of terms made by various rules. We propose a sufficient condition of ET program termination that proves termination by checking each rule in a given program. We also provide an algorithm for this check.

Converting Constraint Handling Rules to Equivalent Transformation Rules

2006 ◽  
Vol 10 (3) ◽  
pp. 339-348 ◽  
Author(s):  
Yoshinori Shigeta ◽  
◽  
Kiyoshi Akama ◽  
Hiroshi Mabuchi ◽  
Hidekatsu Koike ◽  
...  
Keyword(s):  
Constraint Handling ◽  
Equivalent Transformation ◽  
Model Computation ◽  
Computation Model ◽  
Knowledge Processing ◽  
First Order ◽  
Transformation Rules ◽  
Logical Equivalence

We present a way to convert constraint handling rules (CHRs) to equivalent transformation rules (ETRs) and demonstrate the correctness of the conversion in equivalent transformation (ET) theory. In the ET computation model, computation is regarded as equivalent transformations of a description. A description is transformed successively by ETRs. Extensively used in the domain of first-order terms, the ET computation model has also been applied to knowledge processing in such data domains as RDF, UML, and XML. A CHR is a multiheaded guarded rule that rewrites constraints into simpler ones until they are solved. CHRs and ETRs are similar in syntax but they have completely different theoretical bases for the correctness of their computation. CHRs are based on the logical equivalence of logical formulas, while ETRs are based on the set equivalence of descriptions. We convert CHRs to rules used in the ET model and demonstrate converted rules to be correct ETRs, i.e., they preserve meanings of descriptions. We discuss correspondences and differences between CHRs and ETRs in theories, giving examples of correct ETRs that cannot be represented as CHRs.

Formalization of the Equivalent Transformation Computation Model

2006 ◽  
Vol 10 (3) ◽  
pp. 245-259 ◽  
Author(s):  
Kiyoshi Akama ◽  
◽  
Ekawit Nantajeewarawat ◽  
Keyword(s):  
Program Synthesis ◽  
Background Knowledge ◽  
Basic Structure ◽  
Equivalent Transformation ◽  
Computation Model ◽  
Problem Domain ◽  
Central Importance ◽  
Program Correctness ◽  
Transformation Rules ◽  
Successive Reduction

In the equivalent transformation (ET) computation model, a specification provides background knowledge in a problem domain and defines a set of queries of interest. A program is a set of prioritized transformation rules, and computation consists in successive reduction of queries using meaning-preserving transformation with respect to given background knowledge. We present a formalization of the ET model from the viewpoint of program synthesis, where not only computation but also program correctness and correctness relations are of central importance. The notion of program correctness defines “what it means for a program to be correct with respect to a specification,” and a correctness relation provides guidance on “how to obtain such a program.” The correctness relation of the ET model is established, based on which how the basic structure of the ET model facilitates program synthesis is discussed together with program synthesis strategies in this model.

A Logically Justified Model of Computation I

1981 ◽  
Vol 4 (1) ◽  
pp. 151-172
Author(s):  
Pierangelo Miglioli ◽  
Mario Ornaghi
Keyword(s):  
Computer Science ◽  
Program Synthesis ◽  
Completeness Theorem ◽  
Point Of View ◽  
Program Execution ◽  
Computation Model ◽  
Clear Explanation ◽  
Direct Interpretation ◽  
Adequacy Condition ◽  
General Explanation

The aim of this paper is to provide a general explanation of the “algorithmic content” of proofs, according to a point of view adequate to computer science. Differently from the more usual attitude of program synthesis, where the “algorithmic content” is captured by translating proofs into standard algorithmic languages, here we propose a “direct” interpretation of “proofs as programs”. To do this, a clear explanation is needed of what is to be meant by “proof-execution”, a concept which must generalize the usual “program-execution”. In the first part of the paper we discuss the general conditions to be satisfied by the executions of proofs and consider, as a first example of proof-execution, Prawitz’s normalization. According to our analysis, simple normalization is not fully adequate to the goals of the theory of programs: so, in the second section we present an execution-procedure based on ideas more oriented to computer science than Prawitz’s. We provide a soundness theorem which states that our executions satisfy an appropriate adequacy condition, and discuss the sense according to which our “proof-algorithms” inherently involve parallelism and non determinism. The Properties of our computation model are analyzed and also a completeness theorem involving a notion of “uniform evaluation” of open formulas is stated. Finally, an “algorithmic completeness” theorem is given, which essentially states that every flow-chart program proved to be totally correct can be simulated by an appropriate “purely logical proof”.

ON THE UNIQUENESS OF $ \beta\delta $-NORMAL FORM OF TYPED $ \lambda $-TERMS FOR THE CANONICAL NOTION OF $ \delta $-REDUCTION

2019 ◽  
Vol 53 (1 (248)) ◽  
pp. 37-46
Author(s):  
D.A. Grigoryan
Keyword(s):  
Normal Form ◽  
Programming Languages ◽  
Functional Programming ◽  
Sufficient Condition ◽  
Necessary And Sufficient Condition ◽  
Functional Programming Languages ◽  
Monotonic Functions ◽  
Necessary And Sufficient

In this paper we consider a substitution and inheritance property, which is the necessary and sufficient condition for the uniqueness of $ \beta\delta $-normal form of typed $ \lambda $-terms, for canonical notion of $ \delta $-reduction. Typed $ \lambda $-terms use variables of any order and constants of order $ \leq 1 $, where the constants of order 1 are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notion of $ \delta $-reduction is the notion of $ \delta $-reduction that is used in the implementation of functional programming languages.

How to Make Programs from Problem Descriptions in the Equivalent Transformation Paradigm

2003 ◽  
Vol 7 (3) ◽  
pp. 260-267
Author(s):  
Takahiko Ishikawa ◽  
◽  
Kiyoshi Akama ◽  
Hiroshi Mabuchi ◽  
◽  
...  
Keyword(s):  
Problem Solving ◽  
Expressive Power ◽  
Equivalent Transformation ◽  
Sample Problem ◽  
Computation Model ◽  
Transformation Rules ◽  
Manipulative Techniques

In the computation model of equivalent transformation (ET), problems are expressed by some declarative descriptions. Programs, which consist of equivalent transformation rules (ETRs), are made from the declarative descriptions, and applied to questions to solve them. The ET model can achieve various and efficient ways of problem-solving mainly due to the expressive power and priorities of ETRs. In this paper, we investigate and demonstrate, by solving a sample problem, how to make programs from problem descriptions in the ET paradigm. We introduce basic methods of generation and improvement of rules seeking for desirable ETRs. We can transform ETRs, preserving correctness of computation, through many manipulative techniques, i.e., changing from nondeterministic atoms into sequentially executable atoms, introducing multi-head rules, and adjusting priority of rules, by which we can effectively improve correct programs into both correct and more efficient programs.

Constructive mathematics and computer programming

1984 ◽  
Vol 312 (1522) ◽  
pp. 501-518 ◽  
Keyword(s):  
Computer Science ◽  
Programming Languages ◽  
Programming Language ◽  
Program Synthesis ◽  
Constructive Mathematics ◽  
Inference Rules ◽  
Computing Science ◽  
Intuitionistic Theory ◽  
The Difference ◽  
Correct Program

If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation that it is the computer’s duty to execute (a difference that Dijkstra has referred to as the difference between computer science and computing science), then it no longer seems possible to distinguish the discipline of programming from constructive mathematics. This explains why the intuitionistic theory of types (Martin-Lof 1975 In Logic Colloquium 1973 (ed. H. E. Rose & J. C. Shepherdson), pp. 73- 118. Amsterdam: North-Holland), which was originally developed as a symbolism for the precise codification of constructive mathematics, may equally well be viewed as a programming language. As such it provides a precise notation not only, like other programming languages, for the programs themselves but also for the tasks that the programs are supposed to perform. Moreover, the inference rules of the theory of types, which are again completely formal, appear as rules of correct program synthesis. Thus the correctness of a program written in the theory of types is proved formally at the same time as it is being synthesized.

scholarly journals On Unfolding for Programs Using Strings as a Data Type

10.29007/m8rr ◽  
2018 ◽  
Author(s):  
Andrei Nemytykh
Keyword(s):  
Programming Languages ◽  
Term Rewriting ◽  
Computation Model ◽  
Abstract Machine ◽  
Rewriting Systems ◽  
Word Equation ◽  
Semantic Tree ◽  
Long Time ◽  
One Step ◽  
Transformation Methods

As a rule, program transformation methods based on semantics unfolda semantic tree of a given program. Sometimes that allows to optimize the program or to prove its certain properties automatically.Unfolding is one of the basic operations, which is a meta-extension of one step of the abstract machine executing the program.This paper is interested in unfolding for programs based on pattern matching and manipulating the strings. The corresponding computation model originates from Markov's normal algorithms and extends this theoretical base.Even though algorithms unfolding programs were being intensively studied for a long time in the context of variety of programming languages, as far as we know, the associative concatenation was stood at the wayside of the stream.We define a class of term rewriting systems manipulating with strings anddescribe an algorithm unfolding the programs from the class. The programming language defined by this class is algorithmic complete.Given a word equation, one of the algorithms suggested in this paper results in a description of the corresponding solution set.

A NECESSARY AND SUFFICIENT CONDITION FOR THE UNIQUENESS OF $ \beta\delta $-NORMAL FORM OF TYPED $ \lambda $-TERMS FOR THE CANONICAL NOTION OF $ \delta $-REDUCTION

2019 ◽  
Vol 53 (1 (248)) ◽  
pp. 28-36
Author(s):  
L.E. Budaghyan ◽  
D.A. Grigoryan ◽  
L.H. Torosyan
Keyword(s):  
Normal Form ◽  
Programming Languages ◽  
Functional Programming ◽  
Sufficient Condition ◽  
Necessary And Sufficient Condition ◽  
Functional Programming Languages ◽  
Monotonic Functions ◽  
Necessary And Sufficient

In this paper the canonical notion of $ \delta $-reduction is considered. Typed $ \lambda $-terms use variables of any order and constants of order $ \leq 1 $, where the constants of order 1 are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notion of $ \delta $-reduction is the notion of $ \delta $-reduction that is used in the implementation of functional programming languages. It is shown that for canonical notion of $ \delta $-reduction SI-property is the necessary and sufficient condition for the uniqueness of $ \beta\delta $-normal form of typed $ \lambda $-terms.

Sign in / Sign up

Export Citation Format

Share Document