Arrow Research search

Author name cluster

R.C. Sekar

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

TCS Journal 2001 Journal Article

Automata-driven efficient subterm unification

  • R. Ramesh
  • I.V. Ramakrishnan
  • R.C. Sekar

Syntactic unification has widespread use in computing. There are several operations used in deductive computing such as critical pair generation, paramodulation and narrowing that require unifying a term s with every subterm of another term p. This subterm unification problem can be solved naively by repeatedly unifying s with each subterm of p in isolation. The drawback of doing unification in isolation is that commonality among subterms of p is ignored. We present an algorithm for efficient subterm unification by exploiting this commonality. The central idea used in our algorithm is to reduce the common part computation in unification into a string-matching problem and solve it efficiently using a string-matching automaton. The automaton succinctly captures the commonality between subterms of p. The string-matching approach, in conjunction with two new techniques called bidirectional-reduce and marking enables efficient unification of s with every subterm of p.

Details DOI

I&C Journal 1993 Journal Article

Programming in Equational Logic: Beyond Strong Sequentiality

  • R.C. Sekar
  • I.V. Ramakrishnan

Orthogonal term rewriting systems (also known as regular systems) provide an elegant framework for programming in equational logic. O′Donnell showed that the parallel-outermost strategy, which replaces all outermost redexes in each step, is complete for such systems. Many of the reductions performed by this strategy could be wasteful in general. A lazy normalization algorithm that completely eliminated these wasteful reductions by reducing only "needed redexes" was later developed by Huet and Levy. However, this algorithm required the input programs to be restricted to the subclass of strongly sequential systems. This is because needed redexes do not exist for all orthogonal programs, and even when they do, they may not be computable. It is therefore quite natural to ask whether it is possible to devise a complete normalization algorithm for the entire class that minimizes (rather than eliminates) the wasteful reductions. In this paper we propose a solution to this problem using the concept of a necessary set of redexes. In such a set, at least one of the redexes must be reduced to normalize a term. We devise an algorithm to compute a necessary set for any term not in normal form and show that a strategy that repeatedly reduces all redexes in such a set is complete for orthogonal programs. We also show that our algorithm is "optimal" among all normalization algorithms that are based on left-hand sides alone. This means that our algorithm is lazy (like Huet and Levy′s) on strongly sequential parts of a program and "relaxes laziness minimally" to handle the other parts and thus does not sacrifice generality for the sake of efficiency.

Details DOI
v2026.09.13