* Category type
demonstration category
* Problem and Semantics
Nominal approach provides a mechanism of treating variable binding.
Nominal rewriting is a framework of higher-order rewriting with
variable binding based on nominal approach, which was introduced in
[1] M.Frenandez and M.J.Gabbay,
Nominal rewriting,
Information and Computation, Vol.205, pp.917-965, 2007.
In the rewrite relation given in Definition 47 of [1], the
alpha-equivalence is embedded (condition (3) of the definition).
Our proposal is to exclude this condition from the definition of
rewrite relation and consider Church-Rosser modulo alpha-equivalence.
* Input
Input is a finite list of nominal rewrite rules ([1] Definition 39).
Note that, in [1], a nominal rewrite system is defined as the
equivariant closure of a set of nominal rewrite rules.
Rewrite steps are generated by the equivariant closure of the
given nominal rewrite rules.
* Input format
Input grammar is given as follows. Here, like [1], we use '< >' for
tuples to distinguish from (possible abbreviated) parentheses for
function applications and the argument <> for function applications.
spec ::= ( decl ) spec | e
decl ::= VAR idlist | ATOMS idlist | RULES rulelist | id anylist
idlist ::= e | id idlist
rulelist ::= e | rule | rule , rulelist
rule ::= cntxt |- expr -> expr
cntxt ::= e | id # id | id # id , cntxt
expr ::= id expr | term
term ::= id | perm id | ( expr ) | < > | < exprlist > | [ id ] expr
perm ::= [ swaplist ]
swaplist ::= ( id id ) | ( id id ) swaplist
exprlist ::= expr | expr , exprlist
anylist ::= e | any anylist
any ::= id | , | # | [ | ] | string | ( anylist )
Here id denotes non-empty sequences of characters except
white space, '(', ')', '[', ']', '<', '>', ',', '#' and '"',
and excluding the character sequences '|-', '->', 'VAR', 'ATOMS' and 'RULES'.
The empty string is denoted by e and string denotes sequences of any characters
between double quotes.
Additionally the following constraints are imposed:
- at least one VAR, one ATOMS 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 ATOMS
declaration and vice versa.
- all variables and atoms occurring in rules must be declared.
* Example
(VAR X Y Z)
(ATOMS a b)
(RULES
|- sub <[a]app ,Z> -> app _{,sub <[a]Y,Z>>,
|- sub <[a]a,X> -> X,
|- sub <[a]b,X> -> b,
b#Y |- sub <[a]lam [b]X,Y> -> lam [b]sub <[a]X,Y>
)
}