Term rewrite system for terms of lambda calculus?

Question

Are there term rewrite systems, that can rewrite complex lambda term (with nested function application) into some other lambda terms, I.e. reorde function application and, possibly, introduce new variables and add some additional functions into the final term? Google is no help here, because it says, that lamda calculi itself is term rewriting system? Maybe I should use lamda calculus on the lambda calculus? Any reference would be great, some pointers. I can study the field further myself.

E.g I would like start by complex termi with nested functions Sentence(vp(John, walks)) and end with another complex term walks#(John). There may be or may not be some kind of semantic correspondence between input and output. I am just seek i ng framework and scientific tradition that allows to specify such transformations and execute them.

Answer 1

I think that what you are looking for is called higher-order rewriting. There are systems in which you can define rewrite rules of the form $F\;(\lambda x.\lambda y.C\;X[x,y]) \longrightarrow X[X[t,u],v]$ for example, where $F$ and $C$ denote a function symbol and a constant symbols respectively. Note that here, $X$ denotes a higher-order variable (or meta-variable) of arity $2$. In the left-hand side (or pattern), it can be matched against any term containing only variables of $\{x,y\}$. The matched term is then used to replace the occurrences of $X$ in the right-hand side to apply the rewriting rule.

Note that the only terms that match the rewriting rule above are of the form $F\;(\lambda x.\lambda y.C\;A)$, with $FV(A) \subseteq \{x,y\}$. In this case, the variable $X$ is instantiated with $\hat{A}[-,-]$, which is a kind of context such that $A = \hat{A}[x,y]$.

Answer 2

It's hard to understand what you are looking for, but perhaps you are looking for program transformations.

A famous one is the CPS transform (continuation-passing style), which transforms any lambda term $t$ into a quite different one $t'$, which has a semantics related to that of $t$. E.g., $t'$ might follow the call-by-name evaluation of $t$ (CBN CPS transform) or the call-by-value evaluation (CBV CPS transform).

In the implementation of compilers for functional languages (which usually extend the lambda calculus), you may find many other transformations, usually used to optimize code. "Lambda floating", for instance. Essentially, one can rewrite $\lambda x. g (h y) x$ as ${\sf let}\ z=h y\ {\sf in}\ \lambda x. g z x$ so that $hy$ is only evaluated once, even if the function is called many times. CSE (common subexpression elimination) is another well known program transformation.