Simplify the Group operation return type

[Tpt]

Currently the Group operation return type produces a set of partial functions from keys to solution sequences wih the following definition: Group(exprlist, Ψ) = { ListEval(exprlist, μ) → [ μ' | μ' in Ψ, ListEval(exprlist, μ) = ListEval(exprlist, μ') ] | μ in Ψ }.

However, with this definition all ListEval(exprlist, μ) for a given μ are always associated with the same value. Hence, in the set there is only one partial function for each ListEval(exprlist, μ) value. So, it should be possible to simplify this definition to return only a partial function from keys to solution sequences instead of a set of partial function.

I believe that the definition Group(exprlist, Ψ) = k → [ μ | μ in Ψ, ListEval(exprlist, μ) = k ] should do the job. Edit: not a good solution, see infra.

[hartig]

I think the formula in the definition is correct as is and cannot be simplified as you propose.

I believe that the definition Group(exprlist, Ψ) = k → [ μ | μ in Ψ, ListEval(exprlist, μ) = k ] should do the job.

No. Writing k → ... is not a mathematical structure that can be defined to be the result of Group(exprlist, Ψ). Moreover, it is for a single key only and, in fact, it is even undefined what k is.

However, I notice now that the corresponding text in the definition of the Group operator is actually wrong. The text says that Group produces "a set of partial functions from keys to solution sequences." In fact, Group does not produce a set but only a single partial function.

The formula in the definition presents this partial function as a set of assignments, where every key that is in the domain of the partial function is assigned a sequence of solution mappings. Notice that presenting the partial function as a set of assignments is the same as how we often present solution mappings (e.g., μ = {?x → "hello", ?y → "world"}).

So, the only fix that is needed is to change the text in the definition:
".. producing a set of partial functions from .." → ".. producing a partial function from .."

[Tpt]

So, the only fix that is needed is to change the text in the definition:
".. producing a set of partial functions from .." → ".. producing a partial function from .."

Yes, I agree. It's what should be done.

Some nitpicks on your reply (please ignore, I agree with your conclusion):

No. Writing k → ... is not a mathematical structure that can be defined to be the result of Group(exprlist, Ψ). Moreover, it is for a single key only and, in fact, it is even undefined what k is.

I am using the arrow notation here that is I believe quite common so Group(exprlist, Ψ) = k → [ μ | μ in Ψ, ListEval(exprlist, μ) = k ] means that Group(exprlist, Ψ) is a function that for all key k (with key defined as in the spec) associate with k the solution sequence [ μ | μ in Ψ, ListEval(exprlist, μ) = k ].

However, indeed, it is not a good definition here because it defines the function on all possible keys instead of only defining a partial functions on all keys that exists. And I believe it's something we don't want. So, I agree with your conclusion.

However, I notice now that the corresponding text in the definition of the Group operator is actually wrong. The text says that Group produces "a set of partial functions from keys to solution sequences." In fact, Group does not produce a set but only a single partial function.

I am not sure it's "wrong" per se. Having a set of disjoint partial functions exhibit the same behavior as having a single one. But it's indeed overly complicated.