HRS Format
This format deals with higherorder rewrite systems (HRSs) described in
 R. Mayr and T. Nipkow, HigherOrder Rewrite Systems and their Confluence, Theoretical Computer Science, 192(1):3–29, 1998, doi: 10.1016/S03043975(97)001436
hrs ::= signature (RULES rulelist) [(COMMENT string)] signature ::= (VAR sig) (FUN sig)  (FUN sig) (VAR sig) sig ::= ε  id : type sig type ::= type > type  id  (type) rulelist ::= ε  rule  rule, rulelist rule ::= term > term term ::= id  term(termlist)  term term  \idlist.term  (term) termlist ::= term  term, termlist idlist ::= id  id idlistIn
(FUN sig)
the function symbols of the HRS are
declared, while (VAR sig)
declares the types of the variables that are used in the rules. An
identifier must not occur in both the
(FUN sig)
and
(VAR sig)
declarations,
but all identifiers that occur in the
(RULES rulelist)
declaration
must occur in one of them. To save parentheses the following standard
conventions are used: In type
>
associates to the right. For terms,
application associates to the left, while abstraction associates to the
right. Moreover abstractions extend as far to the right as possible, i.e.,
application binds stronger than abstraction. The algebraic notation
term(termlist)
is syntactic sugar for nested application, i.e.,
t(u,...,v)
is syntactic sugar for
(... (t u) ...) v
; note that due to leftassociativity of
application, s t(u,v)
= (s t)(u,v)
=
(((s t) u) v)
. Finally, the expression \x ...y.s
abbreviates \x. ... \y.s
.
Terms must be typable according to the following rules:
x : σ ∈ VAR f : σ ∈ FUN t : σ > τ u : σ x : σ ∈ VAR t : τ     x : σ f : σ t u : τ \x.t : σ > τ
Terms are modulo αβη. In the interest of userfriendliness
and readability we demand that the rules are given in βnormal form,
but do not impose any restrictions concerning η. Note that the
list of variables declared in (VAR sig)
is not
exhaustive, fresh variables of arbitrary type are available to construct
terms. Left and righthand sides of a rewrite rule must be of the same
base type, but we do not demand that free variables appearing on the right
also occur on the left.
Examples

(FUN abs : (term > term) > term app : term > term > term ) (VAR x : term S : term F : term > term ) (RULES app(abs(\x.F x),S) > F(S), abs(\x.app(S,x)) > S ) (COMMENT untyped lambda calculus with beta and eta)

(FUN 0 : nat s : nat > nat nil : natlist cons : nat > natlist > natlist map : (nat > nat) > natlist > natlist ) (VAR n : nat f : nat > nat h : nat t : natlist ) (RULES map (\n.f n) nil > nil, map (\n.f n) (cons h t) > cons (f h) (map (\n.f n) t) ) (COMMENT map on lists of natural numbers)