Add mechanism for tracking which logical variables belong to which domains in
models that comprise of more than 1 domain. This will include handling
quantifier expressions whose indexes refer to their domains in the cardinality
computation logic - e.g. 'there exists X in Peope: ...'.
Note: Clear todos in CardinalityUtil methods: getForAllIndex() and
getThereExistsIndex() - and possibly remove need for these.
Email thread with Rodrigo with respect to this (7 Aug 2012):
{{{
Hi Rodrigo,
On 8/7/12 10:16 AM, Rodrigo de Salvo Braz wrote:
> Hi Ciaran,
>
> I noticed that several JIRA items were referring to the problem of
> identifying the domains of variables.
>
> My take on the problem is that, once we get to representing things like
> "there is X in People : p(X)", it should be a simple matter.
yes, I'm hoping that will be the case.
> For problems in which the domain is needed, the user must have included them
> in the indexed/quantified input expressions, and from then on they are
> always copied to derivative expressions (I think sometimes we derive
> quantified expressions from intensional sets, for example, in which case
> the domain is copied).
If we enforce this constraint as part of model validation (for those with more
than 1 domain). Then yes, once we have proper support for quantifiers with
index expressions and not just indices and the direct R_card logic is updated
as needed (hopefully not too difficult, this should be relatively
straightforward as there is only one call to R_card in the LBP algorithms and
that in R_lift:
R_basic( singleAlpha ^ R_card(| C |_I))
where I in the | C |_I expression should contain the domains. Then it should
just be a simple lookup of the sort declaration in the model to retrieve the
size (can be unknown but then that's a matter of updating the model if needed).
> From what I understand, your contextual variables
> carry their domains along as well, so the domain will always be
> available in the context, or in the expression itself (for
> indexed/quantified variables).
I hadn't considered this but will take into account.
> Is this how you are seeing the solution too?
Partially, but it is now I'm going to add this email thread as a comment to
JIRA ALBP-199.
>
> Thanks,
>
> Rodrigo
Thanks
--
Ciaran O'Reilly
...
}}}
Additional Notes from Rodrigo as regards this:
{{{
From what you are saying, I gather that you intend to validate the model in
advance, store the domains and lookup in the model later on, but I think that's
not the best approach. For example, it might be that the domain of a certain
variable turns out to be irrelevant, so I would not do a validation in advance
-- the computation may well be robust enough to complete without all domains
present -- although such validation might be something the user might
optionally request for greater safety. Also, the way I am seeing it, there is
no need for a model lookup: the domain information would either be right there
in the context, or in the expression itself (in indices or quantifiers). The
disadvantages I see with model lookup is that it would be more work to
implement, and it is too global; in principle one could have the same variable
name associated with different domains at different points in the algorithm. To
summarize, I think that as soon as we get quantified expressions to properly
carry domain information there will be very little change in the algorithm and
all information will be conveniently locally available.
Thanks,
Rodrigo
}}}
Ciaran O'reilly added a comment - 18/Sep/12 8:17 PM
{{{
- may have to put type information in context it belongs in,
e.g. when standardize apart and have type(X) beforehand would want to change
something like:
{ (on X') ...}
to:
{ (on X' in type(X)) ...}
}}}
Shahin Saadati added a comment - 02/Nov/12 3:06 PM
{{{
This fix is also needed for Index Elimination optimization, which requires a
mechanism to create a new index variable and set their domain size to a given
expression.
The solution I have in mind is to be able to create a new name for a set (e.g.
setX), and add |setX| along with the desired size for it into the global object
in 'process'.
}}}
Ciaran O'reilly added a comment - 05/Nov/12 12:42 PM
Note from Rodrigo as regards this:
{{{
BTW, thinking a bit more about domains changing sizes, perhaps we could achieve
that in a clean way
by introducing equalities of the form |type(Y)| = n to the contextual
constraints of a particular branch,
for n the new size. Then we need some atomic rewriter during simplification
that uses such equalities in
the context and replaces expressions of the |type(.)| by the respective
numbers. Perhaps that's what you
were already talking about, I am not really sure...
}}}
Original issue reported on code.google.com by ctjoreilly@gmail.com on 10 Apr 2013 at 11:44
Original issue reported on code.google.com by
ctjoreilly@gmail.comon 10 Apr 2013 at 11:44