Harry R. Lewis
ABSTRACT
In his thesis Paterson proved that equivalence is decidable for program schemata such that every instruction falls on at most one loop and only monadic function signs appear. Here we remove the restriction on function signs. The problem reduces to that of showing that the numerical exponents which satisfy certain "word equations" over a semigroup of acyclic directed graphs may be characterized by sentences of Presburger arithmetic; these exponents correspond to loop coefficients of the program schemata. The central construction is a finite automaton whose memory is a window of bounded size on an acyclic directed graph corresponding to a solution to such a "word equation".
- R. J. Parikh, On context-free languages, J.ACM 16 (1969), pp. 244-255.Google Scholar
Digital Library
- M. S. Paterson, Equivalence Problems in a Model of Computation, Ph.D. thesis, Cambridge University, 1967; reissued as MIT Artifician Intelligence Lab Memo #1, 1970.Google Scholar
- M. S. Paterson and M. N. Wegman, Linear unification, Proc. 8th ACM Symp. on Theory of Comp., pp. 181-186. Google ScholarDigital Library
Recommendations
On Ianov's Program Schemata
Ianov has defined a formal abstraction of the notion of program which represents the sequential and control properties of a program but suppresses the details of the operations. For these schemata he defines a notion corresponding to computation and ...
Complexity of the satisfiability problem for a class of propositional schemata
LATA'10: Proceedings of the 4th international conference on Language and Automata Theory and ApplicationsIterated schemata allow to define infinite languages of propositional formulae through formulae patterns. Formally, schemata extend propositional logic with new (generalized) connectives like e.g. $\bigwedge^{n}_{i=1}$ and $\bigvee^{n}_{i=1}$ where n is ...
Well-structured program equivalence is highly undecidable
We show that strict deterministic propositional dynamic logic with intersection is highly undecidable, solving a problem in the Stanford Encyclopedia of Philosophy. In fact we show something quite a bit stronger. We introduce the construction of program ...
Comments