Handling theories that define vectors

[balacij]

In SSP, we have many models that describe elements of indexable things as being defined as some expression (which may depend on some other indexable things). For example,

and

Additionally, as of right now, we define related variables & unitals as:

Drasil/code/drasil-example/Drasil/SSP/Unitals.hs

Lines 269 to 281 in 88f8b44

	shrResI = makeUCWDS "shrRes" (cn "resistive shear forces")
	(S "the Mohr Coulomb frictional forces per meter" `S.inThe` phrase zDir +:+
	S "for each slice that describe the limit" `S.of_` phrase mobilizedShear +:+
	S "the slice can withstand before failure")
	(vec cP) forcePerMeterU --FIXME: DUE TO ID THIS WILL SHARE THE SAME SYMBOL AS CSM.shearRes
	-- This is fine for now, as they are the same concept, but when this
	-- symbol is used, it is usually indexed at i. That is handled in
	-- Expr.
	shearFNoIntsl = makeUCWDS "T_i" (cn ("mobilized shear forces " ++ wiif))
	(pluralNP (the mobilizedShear) +:+ S "per meter" +:+ S wiif `S.inThe`
	phrase zDir +:+ S "for each slice")
	(vec cT) forcePerMeterU

However, I think this view of the variables is a bit problematic because it hardcodes the i (which becomes problematic when we embed expressions in each other), does not couple the elements to their carrier (it looks like they are different references entirely), and puts no restrictions on i. I think we will need some sort of meta-ModelKind that takes in another ModelKind and "gives" it a variable for using internally. As a starting point, let's consider <ModelName> (<variable Expr> -> ModelKind) (<variable Expr> -> ConstraintSet), where the ConstraintSet is meant to constrain the input variable, and the internal ModelKind is the real model we're interested in. I think with this model, we would be able to define indexable Equational Models, Realms, and Constraints. For the Models and Realms, we would need to require that the quantity they define is an indexed variable -- this is to avoid situations such as forall i. X := S_i (this is more like a constraint that says forall i. X $= S_i instead).

There are models that currently conflict with this requirement, such as:

I think we can either convert them into these new meta-models as well, or we can remove them entirely and replace them with theoretical variants and create another new "StackedModel" that allows us to stack models over each other for wherever they appear in computations (similar to Haskell's do notation) -- "StackedModel" probably isn't the best name however.

Note: this model definitely has logistical issues and will surely cause issues for code generation, but we will need some sort of model to replace the OthModels in SSP's GDs.

Is there any thoughts on what kind of a model we should build for this? I want to say that it's strictly for "universal quantification over indexable things" but it can definitely be related to many other kinds of models.

[smiths]

@balacij you don't need to worry about breaking the code generated for SSP, since we don't currently generate code for SSP. 😄 The reason we don't generate code is because Drasil doesn't currently understand the indexes.

@JacquesCarette will have more meaningful insight that me, but my thinking is that we want to teach Drasil about sequence datatypes. I believe all of the indexed variables in SSP are sequences of reals (floats). For SSP I don't think we need to understand what vector means; I think we have the simpler case of Drasil understanding what sequence means.

[JacquesCarette]

@smiths is correct that the most fundamental thing that's wrong is that Drasil has no notion of sequence, nor of indexing. We can do vectors "barely".

The first phase of the fix is to figure out "indexable types" and indexing (there are some issues open about that). These are basically a special case of functions, where the index set is discrete instead of continuous. That will get rid of some of the hard-coding of "i", but only part.

The second phase is to figure out "functional definitions". We have a bunch of hacks wrt that in our examples, as a bunch of definitions are actually functions (of time), but this is elided. That too should be fixed. This should finish dealing with the hard-coding of "i".

The third phase will then involve models, where we will have to decide what differences we want to make. Is discrete indexing so different than continuous arguments so as to make a big difference? Personally, I don't think so.

[balacij]

Hmm, ok, this sounds like a good plan. I'll leave this ticket open and look to complete tickets related to the first and second phase first. Thank you!

[balacij]

Skimming through tickets, it seems these are relevant:

• Monotonicity constraints: Simplifying SSP (x,y) Input Variable #295
• Implementing Discrete Sets #356
• Representing a tuple in Expr #1213
• Parameterize decision on how to render indexed vectors #1226
• Add lvalues to GOOL #1715
• Express "exactly equal" constraints #1795
• Express constraints on specific values in a list #1796
• Express constraints involving min/max elements of a list #1797
• Express constraints on every element of a list #1799
• Express constraints on concavity #1800
• Express range constraints where an expression is bounded #1801
• Implement linked lists in GOOL #1998
• Vector representation choice #2117
• Discrete spaces representation choice #2118

[JacquesCarette]

Those all seem 'related', yes. But it's also likely that most will need specific fixes - though the split of Expr into 3 will help all of these a lot.