Browse Prior Art Database

Combining higher-order substitution and closure call

IP.com Disclosure Number: IPCOM000239751D
Publication Date: 2014-Dec-01
Document File: 2 page(s) / 37K

Publishing Venue

The IP.com Prior Art Database

Abstract

Disclosed is a method to automatically convert rewriting rules using substitution into a set of equivalent rules that only use closure call.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 52% of the total text.

Page 01 of 2

Combining higher -

Higher order rewriting systems rely heavily on substitution (also called beta reduction) during the process of term normalization through elementary reduction steps (defined by rewriting rules). The basic substitution algorithm requires traversing the entire term tree in order to locate all possible candidates for substitution . The cost is linear over the number of terms in the tree. Optimization techniques such as weakening or pruning, combined with term sharing, have dramatically increased the substitution speed, but at the cost of additional memory for storing meta data, as well as the cost of maintaining this meta data.

Functional programming languages are characterized by the ability to support closure , function within an environment. Compilers for such languages use various optimization techniques to capture the sub environment for late function evaluation; however, the compilers do not support full substitution.

The novel contribution is a method to automatically convert rewriting rules using substitution into a set of equivalent rules that only use closure call (or also called below, shallow closure). This reduces the need for meta data and of considerably increases the substitution speed by generating specialized code just for executing a given substitution.

The novel method works for translating source level rewriting rules into a simpler set of rewriting rules using closure calls. This translation sometimes requires two steps:


1. Eliminate meta closures (a closure created after substitution)


2. Convert deep closure into shallow closure

Since not all rules should be translated into closure calls , the programmer specifies explicitly which rules need to be translated.

As an example, consider these rewriting rules:

ListReversePick Aux[#index, (#hd;), cnt_ v1¹. #return[cnt_, v1¹]] → #retur...