Confluence Competition

HRS Format

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

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:

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)