Redesign of TMs

[samm82]

As mentioned in bf2509d#r34032965, on branch swhsTMs:

I think the current TM definition is quite broken. My new work-in-progress tmEqn passes in the same quantity multiple times, which demonstrates a design flaw. I think the definition of a Theory should be:

data TheoryModel = TM 
  { _mk   :: ModelKind
  , _vctx :: [TheoryModel]
  , _spc  :: [SpaceDefn]
  , _dfun :: [QDefinition]
  , _ref  :: [Reference]
  ,  lb   :: ShortName
  ,  ra   :: String
  , _notes :: [Sentence]
  }

where ModelKind would hold the QDefinition (or RelationConcept). While the _vctx :: [TheoryModel] and _spc :: [SpaceDefn] fields are currently always initialized to be empty (by the constructors), I'm pretty sure that they're to be implemented in the future, so I'll leave them be. My only other uncertainty is _dfun :: [QDefinition] - it is always an empty list when the constructors are called in the examples, and I'm not sure what its purpose is, so we might be able to remove it.

Related to #1373.

UPDATE

Start reading from the last post on this issue

[JacquesCarette]

Ok, what is needed is a proper description of what a theory model is, and what are all its pieces. Currently that is

• what concept is it defining? (current _con)
• what are the theories that need to be defined for this one to make sense? (_vctx)
• what spaces are being defined by this theory? (_spc)
• what (data) definitions are needed for this theory to make sense? (_dfun)
• what operations are being defined by this theory? (_ops)
• what quantities are being declared by this theory? (_quan)
• what quantities are being defined by this theory? (_defq)
• what invariants hold in this theory? (_invs)
• where is this information from? (_ref)
• shortname
• reference address
• notes

That reflects a very general notion of Theory (that basically comes from MathScheme). Overly general for our purpose.

But to understand what to go to next, we really ought to understand every call to tm and tmNoRefs. I don't think there are so many, so I think it's worth doing.

[muhammadaliog3]

Overview of Architecture

Data Definitions: These define actual data with concrete names, symbols and units that are used to build the instance models.

Theory Models: Is a model that defines and relations between data with abstract symbols (rather than concrete symbols defined in data definitions). These relations can be intermediates and do not have to be the final outputs.

General Definitions: I am not quite sure, but I believe it " collects the laws and equations" from the Theory Models

Instance Models: Links the concrete symbols to the theory models to actually obtain the outputs.

In other words IM = DD+TM+GD

Problem: We would like our Theory Models to collect knowledge, generate some additional knoweldge, and store that additional knowledge.

Question 1: What knowledge would we like the Theory models to collect?
I think this is for the most part completed, what we are rather looking for is organizing the knowledge.

• However for data definitions we need a way to express multiple/simultaneous equations.

Question 2: What knowledge would we like Theory Models to generate from the collected knowledge?

• From the raw Expr find out model_type/equation_types: vector or scalar, differential or nondifferential, constrained or not constrained, polynomial or non-polynomial, trigonometric or non-trigonometric, exponential or nonexponential, rational or nonrational, discrete or continuous, complex or real, etc.

A side note:
Here is the list of fields in TM : refby, notes, source, equation, description, and label
Here is the list of fields in data definitions: refby, notes, source, equation, description, units, symbol, label
Here is the list of fields in general definitions: refby, source, description, equation, units, label
Here is the list of fields in instance models: refby, notes, source, description, equations, output constraints, input constraints, output, input, label

A lot of the knowledge in theory models is already stored/captured elsewhere. For example the description section is generated from the Unital chunks. Hence there is not much we could extract from descriptions then what is already found in Unitals.hs.

Likewise I do not think that we should/could extract anything from the notes, as they are very specific and hence not general enough to be used elsewhere.

This meant that the only knowledge that we could extract, has to come from new knowledge that was created for TM/GD/DD/IM (i.e. the relations/expr).

Question 3: How would we store that knowledge? i.e. What does a code solution look like.
I think we should start off with the classifying equation types because of what was advised (take small steps that are easy).

a) First we need to decide if we are looking to classify equations into types (such as vector, differential, etc.) or models into kinds (vector model, differential model, etc.).

b) We would essentially need to create a datatype, relationType or modelKind. Another option is to store the relationType and modelKind as some kind of commonConcept.

c) Make a function to derive the ``relationTypeormodelKind``` or commonconcept from raw expressions and relations.

d) The question is then at what point is the datatype relationType or modelKind derived from the raw expr/relation (this heavily depends on part a).

I will first show the architecture of relations in Drasil
Relation -> RelationConcept -> Field in TM/IM/GD
Meanwhile, for data definitions the architecture is
Expr -> QDefinition -> Field in DD

Here are our potential options

• Store a field in RelationConcept of type relationType or modelKind or commonconcept (this would not work with DD because data definitions do not use RelationConcepts)
• Store a seperate field for relationType or modelKind or commonconcept in TM/IM/GD/DD of type
• Store a single field for relation and relationType in a list of tuples. For example [(f=ma, [Scalar, Nondifferential]) , (a=dv/dt, [Vector, Differential]) ]. This could be done with some variation in TM, IM, GD and DD.

Note that Expr and Relations are synonyms, if that confused you 😃.
haskell type Relation = Expr

Here is the code for Relation Concept just for reference:

data RelationConcept = RC { _conc :: ConceptChunk
                          , _rel :: Relation
                          }

[muhammadaliog3]

With regards to new comments in this issue and in #1174 , I am just going to jot down some new conclusions:

1. we must remove the relationconcept fields in instancemodels, theory models and general definitions and instead use QDefinitions
2. We want to get rid of ExprRelat and just use definingExpr, this also (might) give us an oppurtunity to remove the relToQD.
3. If we are using QDefinitions when we want to have different "definitions" for the various types of equations.

Now 3 solves one of our issues related to this issue, that is we should add a field to QDefinitions to indicate whether if it is a differential, vector, scalar, etc definitions.

[smiths]

Above (#1601 (comment)) @JacquesCarette asked for my notes on the relation between TM/GD/DD/IM. I've thought about it, and looked through my notes, and I cannot think or find anything I can point to. The specific figure relating TM/GD etc was an outcome of a problem that Yuzi was having with circular dependencies. It made sense as a model, so we tried it, and it worked in all our examples, but I don't think we have proven it. We've had plenty of discussions, and conversations are probably scattered through the issue tracker, but I can't think of a specific resource I can point to.

I remember in particular that we discussed this when we discussed "theory specialization." We are currently discussing this under #2195. The TM/GD etc relation is based on experience/common sense. It would be great to try to formalize this somehow has a theory specialization. I think this ties to the challenges of redesigning the TMs. @JacquesCarette is there a good resource on theory specialization that @muhammadaliog3 and I can look at?

[muhammadaliog3]

This was originally 2 posts, one on the relToQd hack and other on the current state of 1601. I have however combined and summarized them. I think I need @smiths for all 4 of them.

1. For equational models, it makes sense to use QDefinitions (because QDefinitions have symbols, units, and spaces). However for non-equational relations we need something else because symbols, units, and spaces don’t have meaning. I would say that we REVERT to RelationConcept for non-equational relations.

2. The difference between a vector equation, a differential equation, and multiequation has to be more then just a label. For example if there is a equation “a=5” there should be some kind of warning, error, or oddity if the user tries to label it as a “differential” equation. Without this the modelKinds seem kind of broken.

We have 3 options

Option A: We could think of a design such that the way we define equation’s should be DIFFERENT depending on what type the equation is.
Option B: We could think of a design such that the way we define qdefinition’s/Model should be DIFFERENT depending on what type the equation is (I know this is not a good example, but if the user was defining a vector we could have them specify the basis).
Option C: Make drasil automatically determine the equation type. (For example we could check if the expr have deriv to determine if the equations are differential).

Number 3 and 4 have to do with the relToQd hack, and I argue that relToQD is not a hack, but rather necessary.

3. In general we need to establish conventions within the model kinds. As of right now however we should only concern ourselves with Equational Models.

The big question is do we include the equal to sign or not in the qdefinitions fr Equational Models. Here are the current conventions

Drasil-examples: Yes the equal to sign is included in the relation.
SRS: Yes the equal to sign is included in the relation.
Generated Code: No the equal to sign is not included in the relation.

Hence because the generated code has different needs, which is why I have concluded that the relToQd hack is needed either in the drasil-gool or drasil-docLang.

For example when I removed the reltoqd hack on friday, and got things to compile (what I had to do is explained in the next question), I noticed with just

pbIsSafeQD :: QDefinition
pbIsSafeQD = ec isSafePb ( sy probBr $< sy pbTol) 

And stable looks like

The generated code comes correct, but the equation display in SRS is incorrect.

Meanwhile if I change the qdefinition and add the equal to sign

pbIsSafeQD :: QDefinition
pbIsSafeQD = ec isSafePb (sy isSafePb $= sy probBr $< sy pbTol)

Then the equation displayed correctly in the SRS, but the generated code does not match stable with the following lines differing return is_safeLR == LR > q when stable says return LR > q

4. For equational models, if there is no relToQD, we need to match the quantityDicts in the QDefinitions correctly, so that drasil can connect with the other equations and determine the getExecOrder. For example, if were to naively define QDefinition as:

pbIsSafeQD =   fromEqn' "safetyReqPb" (nounPhraseSP "Safety Req-Pb")
  EmptyS (Variable "is-safePb") Boolean (sy isSafePb $= sy probBr $< sy pbTol)

Then drasil will not compile. But if were to redefine the QDefinition in terms of the previously declared quantityDict, isSafePb like the following

pbIsSafeQD =  ec isSafePb ( sy probBr $< sy pbTol)

OR just change the UID to match the quantity it is defining like the following

pbIsSafeQD =   fromEqn' "isSafePb" ………..

THEN drasil would compile since it knows how to connect isSafePb to the other equations.

Also note that the FIRST implementation causes differences in the label of the IMOD with the generated SRS. This occurs because the generated SRS just takes the label of isSafePb, while the stable SRS uses the label of IMODS. However this can easily be fixed with a new QDefinition constructor.

[JacquesCarette]

On your two points:

1. Can you give us an example of a non-equational relation that is nevertheless a model? Most of the ones that I know (like those specified by differential equations), it does make sense to have symbols, units and spaces. The one slightly odd one is the 'boolean' one in GlassBR, but it's ok too.
2. I fully agree that it would be best if there was a type system that would disallow broken models. But we're not there (yet), so we will have to approximate. Otherwise it will take too long to implement such a feature. We can help ourselves by only allowing certain models to be built via certain 'smart' constructors that don't allow ill-formed models, and not export the raw constructors. We get a lot of safety already that way.

[As you phrase it, I don't see a big difference between options A and B.]

We want option B:

• different internal representations for each type of model; representation not exposed
• different smart constructors for different kinds

relToQD is a hack. It 'guesses' that a relation is in fact a definition, when it has no right to make that guess. That guess can fail. We need to

1. encode the type of model each of our TM/GD/etc are
2. never guess, because we already have the needed knowledge not to.

We already have ODE models. So we need to implement at least equational, ODE, and 'other'. Where it's fine to basically do nothing with the 'other' ones.

The point is one of knowledge encoding, and one of form (the way an equation looks) versus function (knowing it's just a relation, versus knowing that it is a definition). Math here has its notation wrong. Some PL, have fixed that: some languages use := for assignment, for example, which is way better.

The reason pbIsSafeQD is a big problem, is that it mixes knowledge encoding with display.

Note also that sy isSafePb $= sy probBr $< sy pbTol is kind of ill-typed. I guess if you write it as sy isSafePb $= (sy probBr $< sy pbTol) it's ok again (since isSafePb is of type boolean).

I think you need to ponder the concept of "knowledge capture", and its implications, much more deeply. Your proposed solutions are too close to 'pure code', rather than being based on a broader conceptual understanding of what we're trying to achieve with Drasil. [And we, @smiths and I, are definitely at fault for not having briefed you more deeply about that!]

[muhammadaliog3]

In an attempt to address these issues through knowledge capture I will split this post into 2. The first will be just "knowledge capture" and the second will be related to code.
We currently have 3 problems in this issue.

1. Problem: Representing equilibrium vs representing quantitative definition.

Take a look at this example of "moment equilibrium" relation.

momEqlRel :: Expr
momEqlRel = 0 $= momExpr (\ x y -> x +
  (inxi baseWthX / 2 * (inxi intShrForce + inxiM1 intShrForce)) + y)

Proposed Conceptually: Seperate the meanings of the "equal to" sign

Proposed Code Solution:

Option A: Any equal to sign in an expression should be assumed to mean equilibrium. Definitional equal to signs should be dealt with internally by drasil through the smart constructors. More concretely we should make our models be robust to both QDefinitions and RelationConcepts, where in QDefinitions the definitional equal to sign is added automatically (and define units,symbols and spaces) while the relationConcepts do not modify the expr's in any way (and do NOT define units, symbols and spaces).

Option B: As @JacquesCarette mentioned we could seperate the expr's of ( $= ) into ($:= and $=) .

Option C: Do both A and B

I think option A is the most natural one.

2. The relationship between UID's of equations and the UID of the concept they are defining is unclear and unhelpful.

As an example of this problem, we I will use the example that revealed this problem. pbIsSafeQD revealed that inorder for getExecOrder to work, the UID of the equations = UID of the quantity it is defining the equation for. Say that we were making a QDefinition with defining equation ```sy isSafePb $= ....." , where isSafePb is an already defined unitless quantity, then the UID of the equation must be the same as isSafePb.

Proposed conceptual solution: The identity of the expression is NOT the same as the identity of the quantity being defined in the equation. For example, taking E=mc^2, in science the identity of the equation is "Mass–energy equivalence", not "Energy".

Proposed code solution: Drasil should internally convert the uid of the equation to the uid of the quantity being defined if need be, but they should be kept seperate as often as possible.

[JacquesCarette]

1. We need to be able to represent "assign" and "is equal to". "assign" is asymmetric, and should be represented like that. QDefinition is one reasonable way of doing so. It can be printed as "=", if desired. There is also the 'relation' "is equal to", when two quantities are equal. There are gradations here too: a) two general quantities, b) one quantity is constant, c) one quantity is zero. c) is a special, important case of b), which is a special, important case of a). 'equilibrium' is at a much higher level, and I'm not sure we need to teach Drasil about that yet.

We should, in general, not embed = (or :=) in any of our representations. It does not carry enough meaning to be easily re-usable. That's why, for example, almost all uses of <, <=, > and >= are gone from the examples, replaced by various intervals.

So we need to do something that is kind of like C: for each = in the examples, understand what it actually means, and then rewrite it using a Drasil structure that encodes that meaning (and no other).

2. I agree. It is quite unclear, and that lack of clarity makes it unhelpful. However, every time I encountered a particular situation where things were unclear, I asked [often by opening an issue on here], and each time a clarification was given. Which usually resulted in a code change too.

However, I'm not sure about your conceptual / proposed solution. What I would much prefer to do is to first see 3-4 separate cases where things are unclear (which means 3 or 4 issues), the clarification for each case, and then see if we can extract a general pattern. Experience tells me that it's not quite so simple. I do fully agree there is a problem, and it needs solved. But also that we don't quite have a firm enough grasp of the actual problem, yet.

[muhammadaliog3]

Some examples of PROBLEM_1:

I am not going to show equal to signs being used as assignments, as drasil-example is full of them and I do not think that they are very interesting.

The following are uses of the equal signs that mean more than just assignments.

Some examples of PROBLEM_2:

If we define the QDefinition for the model as

lrIsSafeQD :: QDefinition
lrIsSafeQD = fromEqn' "safetyReqLR" …. (sy isSafeLR $= sy lRe $> sy demand)

We get errors, but if we define it using the same UID of the quantity it is defining

lrIsSafeQD = fromEqn' "isSafeLR" … (sy isSafeLR $= sy lRe $> sy demand)

Everything compiles

If we define the QDefinition for the model as

timeQD :: QDefinition
timeQD = fromEqn "timeRC" …. 
  sy flightDur $= 2 * sy launSpeed * sin (sy launAngle) / sy gravitationalAccelConst

We get errors, but if we define it using the same UID of the quantity it is defining

timeQD = fromEqn "flightduration" …. 
  sy flightDur $= 2 * sy launSpeed * sin (sy launAngle) / sy gravitationalAccelConst

Everything compiles

If we define the QDefinition for the model as

landPosQD :: QDefinition
landPosQD = fromEqn "landPosQD" …  landPosExpr

We get errors, but if we make the uid the same as the uid of the quantity it is defining

landPosQD = fromEqn "landingposition" …  landPosExpr

Everything compiles.

If we define the QDefinition for the model as

offsetQD :: QDefinition
offsetQD = fromEqn "offsetQD" … $ sy offset $= sy landPos - sy targPos

If we make the uid of the the QDefinition the same as the uid of the quantity it is defining,

offsetQD = fromEqn "offset" … $ sy offset $= sy landPos - sy targPos

I hope that these 4 examples can make things clearer.

[muhammadaliog3]

Current State of Theory models:

Empty fields in the theory models in drasil-example: "while the _vctx :: [TheoryModel] and _spc :: [SpaceDefn] fields are currently always initialized to be empty (by the constructors), I'm pretty sure that they're to be implemented in the future, so I'll leave them be." _ops :: [ConceptChunk] and _dfun :: [QDefinition] are always empty, and _defq :: [QDefinition] is empty (except by the relToQD hack in GlassBR)."

Things we want to add to Theory Model/Instance Model/General Definition/Data Definition:

Add ModelKinds
A way to answer "what kind of model is it?" meaning is it a single (scalar) equation lhs = rhs, a vector equation, a differential equation, a set of equations, etc. Note that the same questions hold for InstanceModel. And it is possible that it will be easier to start with InstanceModel then TheoryModel. There are 4 top-level entities in Drasil for holding high-level information like this, and they are related to each other. So even though this issue talks only about TheoryModel, the design needs all 4 to be coherent with each other. So to improve the overall design, we need to understand what kind of "knowledge capture" is being done in each - and what should be done in each.

Fixing Relations

The initial problem was
[It's not that relations are bad, mathematically, it's that we're abusing them in current Drasil to encode things that ought to be encoded in much more precise ways]. We need look at all occurrences of Relation and figure out what they really ought to be instead. Careful: this is a minefield. We'll have to do careful planning before proceeding.

Eventually we determined...
The most fundamental bug in parts of Drasil is that some information of the kind "A = B" where we kind of mean to define A by B, is actually encoded as "A = B", instead of being a definition of the concept A in terms of the 'thing' that B represents. So QDefinition is good, RelationConcept is awful. We need to remove, surgically and one-by-one, each and every use of these 'relations'.

Which translated into the following plan

1. Remove relationconcept, but we want to replace them with a new data-structure that describes different kinds of definitions
2. We want to get rid of ExprRelat class and just use definingExpr, this is very easy
3. Remove the relToQD hack.
4. Define new data structure for various types of qdefinition, that has 3-4 'cases', one of which will be for single equations, and its payload will be a qdefinition. The payload for the other cases still need to be determined and created. For example we can have a DifferentialEquation type with payload QDefiniton, a vector equation type with payload QDefinition, multi equation type with payload [QDefinition]

Which lead to the following problems and potential solutions

• In regards to point 4, is that data structure is implemented there would be a combinatorial explosion of equation types: we have the following classes of equations: vector vs scalar, differential vs nondifferential, singular vs multiple, equational vs nonequational, and complex vs real. However equation can be of multiple types, such as a differential vector equation. This means that if I were to create go the naive way like Dr Carrete said, such as

data ModelKinds = Vector QDefinition | Differential QDefinition | Vector Differential QDefinition ... 

We would end up with 2^5=32 possible options!.

Potential unverified solutions:
First we could do nothing, because most equations are singular we will most likely not need all 2^5 and instead we should just represent the common, OR define the datatype

data equationType = Vector | Differential | Multiple | Equational | Complex
data ModelKinds = Model [equationTypes] [QDefinition]  -- A list of QDefinition is used to incorporate multiple QDefinition

For example Say we have the QDefinitions ["a=g" , "a=dv/dt" , F=ma] then the ModelKinds would be:
Model [Differential, MultiEquational] ["a=g" , "a=dv/dt" , "g = dv/dt"]

• The other 4 problems are stated and explored from the following comment: Redesign of TMs #1601 (comment) All the way down to
  Redesign of TMs #1601 (comment)

[smiths]

Thank you for the summary @muhammadaliog3. Very helpful!

[JacquesCarette]

Yes, both summaries are excellent.

[muhammadaliog3]

@JacquesCarette The following two questions still remain unanswered

1. How are we to encode the difference between equality-as-assignment and equality-as-equilibrium
2. How are we to encode the mapping between equation-uid and the quantity-it-is-defning-uid without relToQd (a reminder that currently reltoqd converts the equation-uid to the uid of the quantity-it-is-defning, right before the code is generated).
   Examples are given in the following comment.

Once these two are answered, I still have to add the modelkinds before I can launch a PR.

[balacij]

I feel like this could be closed in favour of #2599 (and related action items to merge the 3 kinds of theories) and #2853.

[balacij]

Closing in favour of #2599. If anyone feels otherwise, please feel free to re-open.