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
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 -> SThe left- and right-hand side of a rewrite rule must be of the same base type.
- Fresh variables of arbitrary type are available to construct terms (added: 5 August 2018).
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)