MathScheme rename operator: axioms names

[ysharoda]

When the renaming operator is used to change the name of an operation in a theory, the names of the axioms do not reflect that change. For example, the commutativity axiom of semirings has the name commutative*, but defines the commutative property of + operator. ` commutative : ⊢ ∀ [x : U] [y : U] x + y ≐ y + x ` It's more of a problem when considering the theory of rings, as there are associativity axioms for and + The point is to make a place for every symbol that can be renamed in the axiom name, including operations, carriers and unit elements.

[ysharoda]

Another point to discuss mentioned by Dr. Rabe: Should declarations that do not mention all used symbols in the name be rejected?

[florian-rabe]

I think this can be solved with an operation that extends a user-given renaming to an induced renaming.

Assume a given renaming a to r(a) for a in A. Define r'(a) = r(a) if a in A and r'(a) = a otherwise. Then the induced renaming function is R(s1 _ ... sk) = r'(s1) ... _r'(sk).

Is that correct?

[JacquesCarette]

It is important to recall the underlying design that led to this:

1. we want a well-behaved renaming operations
2. we want that post-expansion, the 'path' taken to produce a theory is invisible
3. we would like that post-expanded theories behave just as well as theories produced via combinators.
4. we are in a setting where labels matter (thus the need for renaming)

[Strictly speaking, I would be willing to relax point 3]. The main point is that we need to have a single definition of the commutativity property in the combinator-based library. All other appearances should be because it has been inherited or mixed-in. But, of course, many theories have more than one commutative operator. So we need to have these different properties have different names. But these properties depend, in a non-trivial way, on the name of the operators for which they are a property. [Note: that these are properties is not that crucial, it's just that in mathematics that is where name-dependency shows up more strongly; in a dependently typed system, and also in category theory, this is pervasive].

I should also point out that what is currently implemented in MathScheme works, but is nothing more than a glorious hack. I would be extremely happy to find a principled solution!

One way to think of it would be that commutative should really be commutative(+), where the name is parametrized. Flattening might perhaps then 'wire in' the name, to perhaps commutative_+. [This is why I'm willing to relax point 3].

More importantly, we should really be thinking of theory presentations as telescopes. For telescopes, it is customary to think left/right instead of up/down (like theory presentations are usually shown), where the simplest things are on the left, and more dependent things are on the right. So, in telescopes, everything on the right implicitly depends on all the names on the left. So if we rename something 'in the left', then obviously that should apply to the right as well. In the case of telescopes, the matter is considerably simpler: we don't have names at all, we have positions! So we don't have to rename the field labels, because there are none.

Also, it is indeed important to remember that things like U and ≐ should really be considered to be part of the 'left' of the telescope. It's another part of the MathScheme hack that they are elided, as we don't tend to rename them. That part of the hack is closer to a bug.

[JacquesCarette]

@florian-rabe we were writing at the same time...

So your solution is exactly the hack implemented in MathScheme. It works. It's a hack. I would love to be able to come up with a solid design -- which is why I laid out the situation in more detail above.

[florian-rabe]

Mimicking the hack would be straightforward. (A minor complication is that MMT distinguishes between the name of an operation and the delimiter(s) used in its notation. Users might declare an operation 'plus' with notation + and choose to call the axiom 'commutative_+' or 'commutative_plus'.)

But indeed a more elegant solution would be desirable. Open questions:

• What if an axiom uses many symbols? Does the user have to list them all in the axiom name?
• Are only the symbols occurring in the type relevant? Or also the ones in the definition (if any)?
• What if the user violates the naming convention?

[JacquesCarette]

Yes, that is indeed a complication.

Answers:

• In MathScheme, yes. Or at least, that is the convention. Not enforced.
• All the symbols that occur which are meant to be subject to rename should appear. For properties, that is just the ones in the types (unless you want to rename 'refl' !!); but for definitions, it might indeed be necessary to add the ones there as well.
• Then the results are weird and buggy.

That last point is definitely quite damning wrt this 'solution'.

I do think that telescopes are crucial to a good solution. And for a long time I've been thinking that making theory presentations DAGs rather than totally flat, would help a lot. That way there could be two commutative along two different paths in the DAG [but still shared], and they would be different. In my mind, this is roughly what we're doing with the current naming convention.