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 2 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