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.

available here.

Format

The grammar of the format is given as follows.

spec ::= ( decl ) spec | e
decl ::= VAR idlist | RULES rulelist | FUN idlist | id anylist
anylist ::= e | any anylist 
any ::= id | \ | , | . | : | string | ( anylist )
sig ::= e | id : type sig
rulelist ::= e | rule | rule , rulelist
rule ::= term -> term
term ::= id | term ( termlist ) | term term | \ idlist . term  | ( term )
termlist ::= term | term , termlist
idlist ::= id | id idlist
type ::= type -> type | id | ( type )

Here id denotes non-empty sequences of characters except white space, '(', ')', '"', ',', '\', ':' and '.' and excluding the character sequences '->', 'FUN', 'RULES' and 'VAR'. The empty string is denoted by e and string denotes sequences of any characters.

Additionally the following constraints are imposed:

• At least one VAR, one FUN and one RULES declaration are mandatory. If there are several, the union is taken.
• An identifier declared in a VAR declaration must not be declared in a FUN declaration and vice versa.
• All identifiers occurring in rules must be declared (including bound variables).
• In types -> associates to the right.
• Application associates to the left.
• Abstraction associates to the right.
• Abstractions extend as far to the right as possible (application binds stronger than abstraction).
• Term expression t (u_1,...,u_n) is syntactic sugar for (... (t u_1) ...) u_n note that due to left-associativity of application s t(u,v) = (s t)(u,v) = (((s t) u) v).
• Term expression \ x_1 ... x_n . s is syntactic sugar for \ x_1 . ... \ x_n . s.
• Terms must be typable according to the following rules:

    x : T in VAR      c : T in FUN      s : T -> S    t : T      x : T     s : S
    ------------      ------------      -------------------      ---------------
       x : T              c : T               s t : S             \x.s : T -> S
  

  The left- and right-hand side of a rewrite rule must be of the same base type.

Example

Examples of the format are given below:

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