Equational weighted tree transformations

We consider systems of equations of weighted tree transformations with finite support over continuous and commutative semirings. We define a weighted relation to be equational, if it is a component of the least solution of such a system of equations in a pair of algebras. In particular, we focus on equational weighted tree transformations which are equational relations obtained by considering the least solutions of such systems in pairs of term algebras. We characterize equational weighted tree transformations in terms of weighted tree transformations defined by different weighted bimorphisms. To demonstrate the robustness of equational weighted tree transformations, we give an equational definition of the class of linear and nondeleting weighted top-down tree transformations and of the class of linear and nondeleting weighted extended top-down tree transformations. Finally, we prove that a weighted relation is equational if and only if it is, roughly speaking, the morphic image of a weighted equational tree transformation.     

Forward and backward application of symbolic tree transducers

We consider symbolic tree automata (sta) and symbolic regular tree grammars and their corresponding classes of tree languages: s-recognizable tree languages and s-regular tree languages. We prove that the following three classes are equal: the class of s-recognizable tree languages, the class of s-regular tree languages, and the class of images of classical recognizable tree languages under tree relabelings. Moreover, the sta and the recently introduced variable tree automata are incomparable with respect to their recognition power. Also, we consider symbolic tree transducers (stt) and prove the following theorems. The syntactic composition of two stt computes the composition of the tree transformations computed by each stt, provided that (1) the first one is deterministic or the second one is linear and (2) the first one is total or the second one is nondeleting. Backward application of an stt to any s-recognizable tree language yields an s-recognizable tree language. There is a linear stt of which the range is not an s-recognizable tree language. Forward application of simple and linear stt preserves s-recognizability. A restricted version of both the type checking problem of simple and linear stt, and the inverse type checking problem of arbitrary stt is decidable. Since we deal with trees over infinite alphabets, we require appropriate conditions on sta and stt such that all the proofs are constructive.     

Restricted ground tree transducers

We consider restricted versions of ground tree transducers: total, deterministic, and symmetric subclasses and all other subclasses created by applying any combination of these restrictions. We present the inclusion diagram of the tree transformation classes induced by these restricted ground tree transducers. We show that the following four classes of term relations are the same: (i) tree transformations induced by symmetric deterministic ground tree transducers, (ii) congruence relations on term algebras induced by reduced ground term rewriting systems, (iii) congruence relations on term algebras induced by convergent ground term rewriting systems, and (iv) finitely generated congruence relations on term algebras. As a by-product of our results, we obtain a new ground completion algorithm. Moreover, we show that the following three classes of term relations on term algebras with at least one non-nullary function symbol are also the same: (i) tree transformations induced by total symmetric deterministic ground tree transducers, (ii) congruence relations on term algebras of finite index, (iii) finitely generated congruence relations on term algebras of which the trunk is the whole set of terms.     

About the implementability and the power of equationally defined data abstractions

The question of implementability and expressive power of equational axiom definitions of data abstractions is faced in the paper from the point of view of computability theory.A definition of implementable algebra is given, which looks reasonable and very general. With respect to the given definition it is proved that, if the least congruence semantics is accepted, an equationally defined data algebra is implementable if and only if the least congruence on terms induced by the equational definition is decidable. Moreover, the paper shows that there are: (a) equationally defined data algebras that cannot be implemented; (b) implementable algebras that cannot be expressed in any way by equational axioms.     

The equational theory of Kleene lattices

Languages and families of binary relations are standard interpretations of Kleene algebras. It is known that the equational theories of these interpretations coincide and that the free Kleene algebra is representable both as a relation and as a language algebra. We investigate the identities valid in these interpretations when we expand the signature of Kleene algebras with the meet operation. In both cases, meet is interpreted as intersection. We prove that in this case, there are more identities valid in language algebras than in relation algebras (exactly three more in some sense), and representability of the free algebra holds for the relational interpretation but fails for the language interpretation. However, if we exclude the identity constant from the algebras when we add meet, then the equational theories of the relational and language interpretations remain the same, and the free algebra is representable as a language algebra, too. The moral is that only the identity constant behaves differently in the language and the relational interpretations, and only meet makes this visible.     

Variants of top-down tree transducers with look-ahead

In this article we consider deterministic and strongly deterministic top-down tree transducers with regular look-ahead, with regular check, with deterministic top-down look-ahead, and with deterministic top-down check. We compare the transformational power of these tree transducer classes by giving a correct inclusion diagram of the tree transformation classes induced by them. Along with the comparison we decompose some of the examined classes into simpler classes and we introduce the concept of the deterministic top-down tree automata with deterministic top-down look-ahead. We show that these recognizers recognize a tree language class which is strictly between the class of regular tree languages and the class of tree languages recognizable by deterministic top-down tree automata. We also study the closure properties of the examined tree transformation classes. We show that some classes are closed under composition while others, for example the class of tree transformations induced by deterministic top-down tree transducers with deterministic top-down look-ahead, are not.     

A Finite Equational Axiomatization of the Functional Algebras for the Lambda Calculus

A lambda theory satisfies an equation between contexts, where a context is aλ-term with some “holes” in it, if all the instances of the equation fall within the lambda theory. In the main result of this paper it is shown that the equations (between contexts) valid in every lambda theory have an explicit finite equational axiomatization. The variety of algebras determined by the above equational theory is characterized as the class of isomorphic images of functional lambda abstraction algebras. These are algebras of functions and naturally arise as the “coordinatizations” of environment models or lambda models, the natural combinatory models of the lambda calculus. The main result of this paper is also applied to obtain a completeness theorem for the infinitary lambda calculus recently introduced by Berarducci.     

Functional linear regression after spline transformation

Functional linear regression has been widely used to model the relationship between a scalar response and functional predictors. If the original data do not satisfy the linear assumption, an intuitive solution is to perform some transformation such that transformed data will be linearly related. The problem of finding such transformations has been rather neglected in the development of functional data analysis tools. In this paper, we consider transformation on the response variable in functional linear regression and propose a nonparametric transformation model in which we use spline functions to construct the transformation function. The functional regression coefficients are then estimated by an innovative procedure called mixed data canonical correlation analysis (MDCCA). MDCCA is analogous to the canonical correlation analysis between two multivariate samples, but is between a multivariate sample and a set of functional data. Here, we apply the MDCCA to the projection of the transformation function on the B-spline space and the functional predictors. We then show that our estimates agree with the regularized functional least squares estimate for the transformation model subject to a scale multiplication. The dimension of the space of spline transformations can be determined by a model selection principle. Typically, a very small number of B-spline knots is needed. Real and simulation data examples are further presented to demonstrate the value of this approach.     

Completion of Rewrite Systems with Membership Constraints Part I: Deduction Rules

We consider a constrained equational logic where the constraints are membership conditions t∈swheresis interpreted as a regular tree language. Our logic includes a fragment of second-order equational logic (without projections) where second-order variables range over regular sets of contexts. The problem with constrained equational logics is the failure of the critical pair lemma. This is the reason why we propose new deduction rules for which the critical pair lemma is restored. Computing critical pairs requires, however, solving some constraints in a second-order logic with membership constraints. In a second paper we give a terminating set of transformation rules for these formulas, which decides the existence of a solution, thus showing a new term scheme unification algorithm.Since an order-sorted signature is nothing but a bottom–up tree automaton, order-sorted equational logic falls into the scope of our study; our results show how to perform order-sorted completion without regularity and without sort-decreasingness. It also shows how to perform unification in the order-sorted case, with some higher-order variables (without any regularity assumption).     

Linearity and nondeletion on monadic context-free tree grammars

In this paper, subclasses of monadic context-free tree grammars (CFTGs) are compared. Since linear, nondeleting, monadic CFTGs generate the same class of string languages as tree adjoining grammars (TAGs), it is examined whether the restrictions of linearity and nondeletion on monadic CFTGs are necessary to generate the same class of languages.     

A Microcomputer Based System for Small Relation Algebras

Algebras of n-ary relations are a useful tool in the investigation of logics with limited resources; for example, the equational logic of Tarski's relation algebras corresponds to the three variable fragment of first order logic. We present a computer system which assists in the generation and investigation of properties of relation algebras.     

Proof Transformation via Interpretation Functions: Results, Problems and Applications

Change is a constant factor in Software Engineering process. Redesign of a class structure requires transformation of the corresponding OCL constraints. In a previous paper we have shown how to use, what we call, interpretation functions for transformation of constraints. In this paper we discuss recently obtained results concerning proof transformations via such functions. In particular we detail the fact that they preserve proofs in equational logic, as well as proofs in other logical systems like propositional logic with modus ponens or proofs using resolution rule. Those results have direct applications to redesign of UML State Machines and Sequence Diagrams. If states in a State Machine are interpreted by State Invariants, then the topological relations between its states can be interpreted as logical relations between the corresponding formulas. Preservation of the consequence relation can bee seen as preservation of the topology of State Machines. We indicate also an unsolved problem and discuss the mining of its positive solution.     

A transformation system for concurrent processes

Program transformation techniques have been extensively studied in the framework of functional and logic languages, where they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention. In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented” to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information. Received: 24 April 1997 / 19 November 1997     

On Action Logic: Equational Theories of Action Algebras

Pratt (1991, Proceedings of JELIA’90, Volume 478, pp.97–120) defines action algebras as Kleene algebras withresiduals and action logic as the equational theory of actionalgebras. In contrast to Kleene algebras, action algebras forma (finitely based) variety. Jipsen (2004, Studia Logica, 76,291–303) proposes a Gentzen-style sequent system for actionlogic but leaves it as an open question if this system admitscut-elimination and if action logic is decidable. We show thatJipsen's system does not admit cut-elimination. We prove thatthe equational theory of *-continuous action algebras and thesimple Horn theory of *-continuous Kleene algebras are not recursivelyenumerable and they possess FMP, but action logic does not possessFMP.     

Linearisation: An optimisation for nonlinear functional programs

Functional programming languages have great appeal from the point of view of both software design and amenability to formal reasoning, but to date they have suffered from poor performance when run on conventional computers. A promising solution to this problem may be provided by program transformation and several schemes have been proposed which can give quite impressive optimisations. However, these are at best only semi-automatic, requiring reasoning on behalf of the programmer to assist the transformation process. Part of the problem is that these schemes must take into account not only functions but also the objects to which they are applied in the defining expressions. By reasoning at the function level, the auxiliary domain of objects need not be considered explicitly, and transformations can be derived in terms of identities between functional expressions, rather than via sets of equations satisfied by objects from a certain class.

By expressing functional expressions in variable-free form, we use algebraic methods, based on the functional algebra of the language FP, to transform a certain class of nonlinear functions into linear form. A function in this class generates a reduction graph in the form of a balanced tree when applied to an argument, whereas a linear function generates a single-spine tree and so executes with a number of function calls which is linear in the size of its argument. Thus, for example, tail recursive functions form a small subset of the class of linear functions. Further optimisations include the tupling of functions which are defined by mutal recursion, and we identify conditions under which these are equivalent to a linear function. The compiler is able to detect if the conditions required by these transformation theorems are satisfied, and generate the appropriate optimised functions.     

States on <Emphasis Type="Italic">R</Emphasis><Subscript>0</Subscript> algebras

The aim of this paper is to introduce the notion of states on R ₀ algebras and investigate some of their properties. We prove that every R ₀ algebra possesses at least one state. Moreover, we investigate states on weak R ₀ algebras and give some examples to show that, in contrast to R ₀ algebras, there exist weak R ₀ algebras which have no states. We also derive the condition under which finite linearly ordered weak R ₀ algebras have a state. This work is supported by NSFC (No.60605017).     

An Equational Axiomatization of Dynamic Negation and Relational Composition

We consider algebras on binary relations with two main operators: relational composition and dynamic negation. Relational composition has its standard interpretation, while dynamic negation is an operator familiar to students of Dynamic Predicate Logic (DPL) (Groenendijk and Stokhof, 1991): given a relation R its dynamic negation R is a test that contains precisely those pairs (s,s) for which s is not in the domain of R. These two operators comprise precisely the propositional part of DPL.This paper contains a finite equational axiomatization for these dynamic relation algebras. The completenessresult uses techniques from modal logic. We also lookat the variety generated by the class of dynamic relation algebras and note that there exist nonrepresentable algebras in this variety, ones which cannot be construedas spaces of relations. These results are also proved for an extension to a signature containing atomic tests and union.     

Valid transformations: a new class of loop transformations forhigh-level synthesis and pipelined scheduling applications

In this paper we present a new class of loop optimizing transformations called valid transformations, which are suitable for fine-grain parallelization applications such as high-level synthesis of VLSI designs or compilers for super-scalar or VLIW machines. This class of transformations are different from existing ones in that valid transformations can be illegal. Nevertheless, if a transformation is valid, the transformed loop has a feasible pipeline schedule. We present an example valid transformation called loop expansion which can help produce cost-performance efficient designs and explore a larger design space for a satisfactory design. Several examples are used to demonstrate the efficacy of the proposed technique     

Modular Higher-Order Equational Preunification

Preunification of simply typed λ-terms with respect to the equivalence relation induced by α-, β- and η-conversion and an arbitrary first-order equational theory is useful in higher-order proof and logic programming systems. In this paper we present a procedure for such preunification, which is based on three transformations and parameterized by a first-order equational unification procedure that admits free function symbols. The procedure is proved to be sound and complete, provided that the parameterizing procedure is.     

The Complexity of Counting Problems in Equational Matching

We introduce a class of counting problems that arise naturally in equational matching and investigate their computational complexity. If E is an equational theory, then #E-Matching is the problem of counting the number of most general E-matchers of two given terms. #E-Matching is a well-defined algorithmic problem for every finitary equational theory. Moreover, it captures more accurately the computational difficulties associated with finding minimal complete sets of E-matchers than the corresponding decision problem for E-matching does.In 1979, L. Valiant developed a computational model for measuring the complexity of counting problems and demonstrated the existence of #P-complete problems, i.e., counting problems that are complete for counting non-deterministic Turing machines of polynomial-time complexity. Using the theory of #P-completeness, we analyze the computational complexity of #E-matching for several important equational theories E. We establish that if E is one of the equational theories A, C, AC, I, U, ACI, Set, ACU, or ACIU, then #E-Matching is a #P-complete problem. We also show that there are equational theories, such as the restriction of AC-matching to linear terms, for which the underlying decision matching problem is solvable in polynomial time, while the associated counting matching problem is #P-complete.