Associative, commutative properties and identity elements of non-binary functions

Question

I'm making a compiler (for a new language) wich supports AC unification via pattern matching. The matching algorithms already works but i'm having trouble with the logical and mathematical aspects of functions and it's properties, wich will define in great ways the design of the language. I have several questions about function properties:

Associative and commutative properties apply only on binary functions?

for example if i declare a function max(a,b), this will be commutative because max(a,b) = max(b,a) and associative because max(a,max(b,c)) = max(max(a,b), c), but i can't think of any function with more than two arguments that satisfy this axioms. For example i can define max(a,b,c) = max(a,max(b,c)) which will be a ternary function but the language will be able to unify it with the binary operations that conforms it.

The unification works by reducing associative functions such as max(a,max(b,c)) onto a varydic and canonical form max(a,b,c) and then performing the pattern matching onto this canonical forms, so all (i think) posible functions that have this properties with more than 3 arguments are in fact composites of the same binary function

Do identity elements apply only on binary functions?

Explanaition: There can be a varydic function f(a,b,...) (more than 2 arguments) such that exist an element e that satisfies f(a,b,c,e) = f(a,b,c) for functions that doesn't have an immediate binary parent (such as addition is binary but the compiler manages addition as a varydic function for internal representantion)

Unitiy elements such as zero in addition are managed in the language only by removing its aparences on functions for example add(1,2,x,0) wich represents the expression 1+2+x+0 reduces to 1+2+x

This questions are decisive for the design of algorithms that automatically identify this properties on functions when rules are defined such as a+b = b+a and for the language design and the constraints that will impose to the declaration of functions, which can be, if false for any of this questions, illogical

Answer 1

One way to look at AC and varyadic functions is to look at the cons function for lists, bags and sets:

 cons(a, cons(b, nil)) // depicts a binary tree, a list or a set?

• If cons has no axioms, then it is a binary tree
• If cons is associative, and not commutative and not idempotent, then it is a list.
• If cons is associative and commutative, then it is a bag
• If cons is associative and commutative and idempotent, then it is a set.

Now, varyadic functions act like better notations for cons:

• set(1,2,3,4) is a "better notation" for cons which is ACI.
• list(1,2,3,4,1,2,3,4) for A
• bag(1,1,2,2,3,3,4,4) for AC

Systems such as ELAN, Maude, Tom, ASF+SDF, which support some sort of "matching modulo", use this congruence under the hood: they map binary operators with theories to internal data-structures such as lists, sets, and bags by flattening recursive applications, ordering and eliminating duplicates etc.