On logic of complex algorithms

An algebraic approach to programs called recursive coroutines — due to Janicki 3] — is based on the idea to consider certain complex algorithms as algebraics models of those programs. Complex algorithms are generalizations of pushdown algorithms being algebraic models of recursive procedures (see Mazurkiewicz 4]). LCA — logic of complex algorithms — was formulated in 11]. It formalizes algorithmic properties of a class of deterministic programs called here complex recursive ones or interacting stacks-programs, for which complex algorithms constitute mathematical models. LCA is in a sense an extension of algorithmic logic as initiated by Salwicki 14] and of extended algorithmic logic EAL as formulated and examined by the present author in 8], 9], 10]. In LCA — similarly as in EAL-ω ⁺ -valued logic is applied as a tool to construct control systems (stacks) occurring in corresponding algorithms. The aim of this paper is to give a complete axiomatization. of LCA and to prove a completeness theorem. Logic of complex algorithms was presented at FCT'79 (International Symposium on Fundamentals of Computation Theory, Berlin 1979)