Calculation of Fundamental Groups via Computational Paths

We address the question as to how to formalise the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. The intention is to demonstrate the use of a term rewriting system in performing computations with these computational paths, establishing equalities between equalities, and further higher equalities, in particular, in the calculation of fundamental groups of surfaces such as the circle, the torus and the real projective plane.

A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting

In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compositionally all possible rewritings of a term rewriting system. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom-up fixpoint characterization.We prove soundness and completeness w.r.t. the small-step behavior of rewriting for the full class of term rewriting systems.

Computer Aided Verification of Relational Models by Strategic Rewriting

Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by point-free binary relational expressions, proof obligations can be expressed as inclusions between relational expressions. We developed a typedirected, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.