
I once tried enumerating smallest <CIC inductive definition, binary_fn> terms that satisfy some given algebraic laws. Beyond obvious stuff like the (+,*) integer ring, there were some cool tree-like objects but otherwise nothing groundbreaking.
Taelin@VictorTaelin
I think important functions like add, mul, sort have many short extensionally equivalent definitions, while unimportant functions like f(x)=24*x-7 do not, and that gives us a direct way to rank functions by importance (?)
English









