Definition, syntax and token for "setting a component of an extensible structure" (df-sets)

[benjub]

Digging into my emails with Norm, I found this topic I had discussed with him, Gérard and Mario. I had made the following proposal, which I still support.

The current definition of sSet, which denotes "setting components of an extensible structure",

csts $a class sSet $.
df-sets $a |- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) ) $.

First, sSet is too reminiscent of "simplicial set" and should be changed. Adapting a proposal from Mario, I proposed the following definition:

$a class [ B / A ]s S $.
$a |- [ B / A ]s S = ( ( S |` ( _V \ ( A ` ndx ) ) u. { <. ( A ` ndx ) , B >. } ) $.

This could be displayed as $[ B / A ]_{mathrm{struct}} S$ and is purposefully reminiscent of the syntax for substitution. I think this renders the reading, human parsing and understanding easier.

It is generally better to define new constructions as class constants, e.g. class sin versus class sin A. I think this is indeed important whenever the defined term is a mathematical object, like sin. But here, I don't see what would be gained by considering "setting a component of an extensible structure" as a mathematical object.

This change of df-sets would entail some local changes, but, at first sight, nothing too large. Strictly speaking, the current df-sets may set several components at once, but I do not know if this feature is used often, and I think [ . / . ]s . can be used twice or thrice in a row anyway, and that this may even be clearer.

What do people think ?

[avekens]

I like the proposed new notation setting/sustituting a component of a structure, at least from a display point of view.. Since the second argument is (almost) always an ordered pair (is there any reason/application for something else?) it makes sense to move this into the definition, as proposed. Although the comment of df-sets says "Set one or more components of a structure", I think there is no way to set more than one component simultaneously, at least I found no example for it. Therefore, this should be no problem.

What is still to be considered are the cases for A, B or S being proper classes and not sets (as assured by the current definition) - is the definition still meaningful or at least does not produce harmful results?

The advantage of the current definition is that the basic library theorems (for equality, explicit/implicit class substitution, not free variables, etc.) need not be provided because they are already available by the maps-to notation.

[avekens]

PS: an example for sustituting 2 components is ~tngval: tngval $p |- ( ( G e. V /\ N e. W ) -> T = ( ( G sSet <. ( dist `` ndx ) , D >. ) sSet <. ( TopSet `` ndx ) , J >. ) ) $= I think, however, that this can be translated into a nested square bracket construct with the new notation.

[benjub]

As for setting several components at once, that is the topic of my last paragraph above, and using expressions like [ B / *r ]s [ A / +g ]s S seems acceptable. By the way: tngval also uses sSet twice in a row, while it could have been written T = ( G sSet { <. ( dist `` ndx ) , D >. , <. ( TopSet `` ndx ) , J >. } )

As for classes instead of sets, this may add (/) to a structure, because a couple having a proper class as a component is currently coded in set.mm to be the empty set (if it were coded to be a proper class, like in ~bj-2uplex, then nothing would be added to the structure). Adding (/) to a structure is innocuous (this is the point of having \ { (/) } in df-struct).

It's a good point that basic equality lemmas would need to be proved from this new construct.

[digama0]

You can't use sSet to set more than one component of the structure at once, because it takes an ordered pair as its second argument, not a set of ordered pairs. (The comment on the definition is incorrect, unless you interpret it as saying that you can set more components by iterating it.)

[david-a-wheeler]

Can we call this something other than "setting a component"?? The word "set" is used all over to mean, well, sets. While it's valid English, using the word in these two very different ways is confusing. I like "assign" or "replace", though other words would also be fine; let's use a different word for this different concept.

I'm with switching to something like the current substitution notation, e.g., [ B / A ]s . However, I think it might be better to make the first token different, instead of the last one, so that humans & computer parsers can more quickly determine that this isn't the "normal" substitution. E.g., [s B / A ] or something like that. Or [a ... if this is considered "assigns".

[benjub]

Then maybe [s A / B ]s S is best (similar to [. A / x ]. ph and [_ A / x ]_ B). As for the wording: [s A / B ]s S is the extensible structure which is like S except that the value A has been put in the slot B (replacing the current value if there was already one). I am less worried about the wording containing "set" than about the token, since in sentences, it is often possible to distinguish the noun "set" from the verb "set" (or to phrase the comment so that it is possible to make the distinction).

[avekens]

I think the "s" in "[ B / A ]s" (or "[ B / A ]s") does not stand for "set", but for "structure" ("substitution in a structure"). This would be analogous to "|`s" ("restriction of a structure").

[benjub]

You're right, and I proposed in my first post above to display it as follows:

This could be displayed as $[ B / A ]_{mathrm{struct}} S$ and is purposefully reminiscent of the syntax for substitution. I think this renders the reading, human parsing and understanding easier.

[david-a-wheeler]

I like [s A / B ]s S it has a very similar analogy to other constructs. The proposed text also make sense to me: "[s A / B ]s S is the extensible structure which is like S except that the value A has been put in the slot B (replacing the current value if there was already one)" - that uses the word "replace" instead of overused word "set" :-).

[benjub]

Thanks @avekens, @digama0, @david-a-wheeler. There are about 100 occurrences of "sSet" in set.mm, most of them of the form ( S sSet <. ( A ` ndx ), B >. ), which we'll have to replace by [s B / A ]s S. In the fewer occurrences of ( S sSet <. A , B >. ) or even ( S sSet A), the whole statement has to be modified so that the theorem state the same thing. I'll see how to handle this best: probably first add the new syntax in addition to the old one, and progressively deprecate the old one (like @avekens recently did with other large changes).