HRS Format

This format deals with higher-order rewrite systems (HRSs) described in

• R. Mayr and T. Nipkow, Higher-Order Rewrite Systems and their Confluence, Theoretical Computer Science, 192(1):3–29, 1998, doi: 10.1016/S0304-3975(97)00143-6

with slight modifications detailed below the typing rules. The format follows the same style as the first-order formats, adding type declarations to variables and function symbols as well as syntax for abstraction and application according to the following grammar:

  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 idlist

In (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 left-associativity 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 user-friendliness 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 right-hand 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

1. (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)
   

2. (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)