Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Thursday 12 January 2006 17:14, Yevgen Voronenko wrote:
> Is it possible to define higher order functions (operators) in Maude
> without resorting to meta-level?
>
> For example, I would like to define a map function (operator).
> using pseudo-notation:
> map : List Func -> List
> map([1, 2, 3], increment) = [increment(1), increment(2), increment(3)]
>
> in the above increment would be a Maude operator.
>
> I was able to defined this using Meta-level, but it seems inefficient
> and overly complicated.

Maude is a first order language, so it only has a first order type system. 
However, as in most term rewriting languages it is a simple matter to define 
an application operator (or the whole untyped lambda calculus if you care), 
and simulate higher order function evaluation (though not higher order 
rewriting). For example:

fmod AP{X :: TRIV} is
  sort Func{X} .
  op _[_] : Func{X} X$Elt -> X$Elt [prec 17] .
endfm

fmod MAP{X :: TRIV}
  inc AP{X} .
  inc LIST{X} .
  var E : X$Elt .
  var L : List{X} .
  var F : Func{X} .
  op map : List{X} Func{X} -> List{X} .
  eq map(nil, F) = nil .
  eq map(E L, F) = F[E] map(L, F) .
endfm

fmod TEST is
  inc MAP{Nat} .
  var N : Nat .
  op inc : -> Func{Nat} .
  eq inc[N] = N + 1 .
endfm

red map(1 2 3 5 7 11 13, inc) .

Steven