Encoding Higher-Order programs into TRSs

We use the defunctionalization technique of J. C. Reynolds. The principle is that every function symbol becomes a constant in the TRS and that we add a unique (and reserved) application symbol "app" encoding function application. For instance the classical "plus" function on natural numbers and the higher-order "map" function on lists are encoded by the following TRS

Ops plus:0 s:1 o:0 app:2 map:0 cons:2 nil:0
Const s o nil cons
Vars X Y F

TRS R
  app(app(plus,o),X) -> X
  app(app(plus,s(X)),Y) -> s(app(app(plus,X),Y))

  app(app(map,F),nil) -> nil
  app(app(map,F),cons(X,Y)) -> cons(app(F,X),app(app(map,F),Y))

SRegexp A0
  app(app(map,app(plus,s(o))),[cons([s(*|o)],*|nil)])

Automaton TC
States qi ql
Final States qi ql
Transitions
   o -> qi
   s(qi) -> qi
   cons(qi,ql) -> ql
   nil -> ql

Patterns
   cons(o,_)
   cons(_,cons(o,_))
   cons(_,cons(_,cons(o,_)))

In this encoding, the term plus(o,s(o)) is replaced by a defunctionalized term app(app(plus,o),s(o)). Here, the initial language A0 is defined, using a simplified regular expression. This language contains terms of the form (map (plus 1) nat_list), i.e., map applied to the partial application of plus on 1 (this is subterm app(plus,s(o))), and on any list of natural numbers.