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