JacquesCarette / Drasil

Generate all the things (focusing on research software)
https://jacquescarette.github.io/Drasil
BSD 2-Clause "Simplified" License
143 stars 26 forks source link

Redesign of TMs #1601

Closed samm82 closed 1 year ago

samm82 commented 5 years ago

As mentioned in https://github.com/JacquesCarette/Drasil/commit/bf2509dcac5e3fde078c988873f64805fe1abdc2#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 commented 5 years ago

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

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.

samm82 commented 5 years ago

Calls to TM Constructors:

All taken from master since this should be done in a separate PR than swhsTMs - let me know if I should look at the swhsTMs branch instead.

The current definition of a TM is:

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-theory/Theory/Drasil/Theory.hs#L29-L42

and the current constructors for TMs are:

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-theory/Theory/Drasil/Theory.hs#L70-L84

drasil-data

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-data/Data/Drasil/Theories/Physics.hs#L21-L25

GamePhysics

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/GamePhysics/TMods.hs#L34-L38

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/GamePhysics/TMods.hs#L58-L66

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/GamePhysics/TMods.hs#L110-L114

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/GamePhysics/TMods.hs#L141-L145

GlassBR

https://github.com/JacquesCarette/Drasil/blob/47941ae0135f68798f5957013743da82c99fa52a/code/drasil-example/Drasil/GlassBR/TMods.hs#L32-L39

https://github.com/JacquesCarette/Drasil/blob/47941ae0135f68798f5957013743da82c99fa52a/code/drasil-example/Drasil/GlassBR/TMods.hs#L53-L60

SSP

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SSP/TMods.hs#L30-L33

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SSP/TMods.hs#L44-L47

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SSP/TMods.hs#L67-L71

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SSP/TMods.hs#L97-L101

SWHS

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SWHS/TMods.hs#L33-L37

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SWHS/TMods.hs#L77-L82

https://github.com/JacquesCarette/Drasil/blob/47050c6081fc3a663b23b69fac0ee7c28679f839/code/drasil-example/Drasil/SWHS/TMods.hs#L142-L145

Analysis

As mentioned above, "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).

muhammadaliog3 commented 4 years ago

Analysis update

samm82 is still correct in the following : """As mentioned above, "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)."""

Here is the updated code, where I first show the theorymodel and then have a line defining what is empty

DRASIL PHYSICS
newtonSL :: TheoryModel
newtonSL = tmNoRefs (cw newtonSLRC)
  [qw QP.force, qw QPP.mass, qw QP.acceleration] ([] :: [ConceptChunk])
  [] [sy QP.force $= sy QPP.mass * sy QP.acceleration] []
  "NewtonSecLawMot" [newtonSLDesc]
Empty -------- c1 dq defn 
What kind of model is it: scalar equation

GAMEPHYSICS

newtonTL = tmNoRefs (cw newtonTLRC) [qw force_1, qw force_2]
  ([] :: [ConceptChunk]) [] [newtonTLRel] [] "NewtonThirdLawMot" [newtonTLNote]
Empty -------- c1 dq defn 
What kind of model is it: vector equation

newtonLUG :: TheoryModel
newtonLUG = tmNoRefs (cw newtonLUGRC)
  [qw force, qw gravitationalConst, qw mass_1, qw mass_2,
  qw dispNorm, qw dVect, qw distMass] ([] :: [ConceptChunk])
  [] [newtonLUGRel] [] "UniversalGravLaw" newtonLUGNotes
Empty -------- c1 dq defn 
What kind of model is it: vector equation

newtonSLR = tmNoRefs (cw newtonSLRRC)
  [qw torque, qw momentOfInertia, qw angularAccel] 
  ([] :: [ConceptChunk]) [] [newtonSLRRel] [] "NewtonSecLawRotMot" newtonSLRNotes
Empty -------- c1 dq defn 

What kind of model is it: looks like vector equation?

pasted image 0

GLASSBR

lrIsSafe :: TheoryModel
lrIsSafe = tm (cw lrIsSafeRC)
   [qw isSafeLoad, qw tmLRe, qw tmDemand] ([] :: [ConceptChunk])
   [relToQD locSymbMap lrIsSafeRC] [sy isSafeLoad $= sy tmLRe $> sy tmDemand] [] [makeCite astm2009] 
   "isSafeLoad" [lrIsSafeDesc]
   where locSymbMap = cdb thisSymbols ([] :: [IdeaDict]) symb
                          ([] :: [UnitDefn]) [] [] [] [] [] [] []
Empty ----------- c1 defn
What kind of model is it: scalar equation AND scalar constraint 

pbIsSafe :: TheoryModel
pbIsSafe = tm (cw pbIsSafeRC) 
  [qw isSafeProb, qw probFail, qw pbTolfail] ([] :: [ConceptChunk])
  [relToQD locSymbMap pbIsSafeRC] [sy isSafeProb $= sy probFail $< sy pbTolfail] [] [makeCite astm2009]
  "isSafeProb" [pbIsSafeDesc]
  where locSymbMap = cdb thisSymbols ([] :: [IdeaDict]) symb
                          ([] :: [UnitDefn]) [] [] [] [] [] [] []
Empty ------------ c1 dfn
What kind of model is it: scalar equation AND scalar constraint 

PROJECTILE

accelerationTM :: TheoryModel
accelerationTM = tm (cw accelerationRC)
  [qw acceleration, qw velocity, qw time] ([] :: [ConceptChunk]) [] [accelerationRel] []
  [makeCite accelerationWiki, makeCiteInfo hibbeler2004 $ Page [7]] "acceleration" []
Empty -------------- c1 dq dfn notes
What kind of model is it: differential equation AND vector constraint 

velocityTM :: TheoryModel
velocityTM = tm (cw velocityRC)
  [qw velocity, qw position, qw time] ([] :: [ConceptChunk]) [] [velocityRel] []
  [makeCite velocityWiki, makeCiteInfo hibbeler2004 $ Page [6]] "velocity" []
Empty -------------- c1 dq dfn nots
What kind of model is it: differential equation AND vector constraint 

SSP

factOfSafety :: TheoryModel
factOfSafety = tm (cw factOfSafetyRC)
  [qw fs, qw resistiveShear, qw mobilizedShear] ([] :: [ConceptChunk])
  [] [factOfSafetyRel] [] [makeCite fredlund1977] "factOfSafety" []
Empty --------------- c1 dq dfn notes
What kind of model is it: scalar equation AND scalar constraint 

equilibrium :: TheoryModel
equilibrium = tm (cw equilibriumRC)
  [qw fx] ([] :: [ConceptChunk])
  [] [eqRel] [] [makeCite fredlund1977] "equilibrium" [eqDesc]
Empty --------------- c1 dq dfn
What kind of model is it: scalar equation AND scalar summation

mcShrStrgth :: TheoryModel
mcShrStrgth = tm (cw mcShrStrgthRC)
  [qw shrStress, qw effNormStress, qw fricAngle, qw effCohesion] 
  ([] :: [ConceptChunk])
  [] [mcShrStrgthRel] [] [makeCite fredlund1977] "mcShrStrgth" [mcShrStrgthDesc]
Empty -------------- c1 dq dfn
What kind of model is it: scalar equation 

effStress :: TheoryModel
effStress = tm (cw effStressRC)
  [qw effectiveStress, qw totNormStress, qw porePressure] 
  ([] :: [ConceptChunk])
  [] [effStressRel] [] [makeCite fredlund1977] "effStress" [effStressDesc]
Empty --------------- c1 dq dfn
What kind of model is it: scalar equation

SWHS

consThermE :: TheoryModel
consThermE = tm consThermERC
  [qw thFluxVect, qw gradient, qw volHtGen, 
    qw density, qw heatCapSpec, qw temp, qw time] ([] :: [ConceptChunk])
  [] [consThermERel] [] [consThemESrc] "consThermE" consThermENotes
Empty -------------- c1 dq dfn
What kind of model is it: vector equation AND differential equation

sensHtE = sensHtETemplate AllPhases sensHtEdesc
data PhaseChange = AllPhases | Liquid
sensHtETemplate :: PhaseChange -> Sentence -> TheoryModel
sensHtETemplate pc desc = tm (sensHtERC pc eqn desc)
  [qw sensHeat, qw htCapS, qw mass, 
    qw deltaT, qw meltPt, qw temp, qw htCapL, qw boilPt, qw htCapV] ([] :: [ConceptChunk])
  [] [eqn] [] [sensHtESrc] "sensHtE" [desc] where
    eqn = sensHtEEqn pc
Empty ---------------- c1 dq dfn
What kind of model is it: Piecewise scalar eqution

latentHtE :: TheoryModel
latentHtE = tm latentHtERC
  [qw latentHeat, qw time, qw tau] ([] :: [ConceptChunk])
  [] [latHtEEqn] [] [latHtESrc] "latentHtE" latentHtENotes
Empty ---------------- c1 dq dfn
What kind of model is it: scalar equation AND differential equation (intergral)

nwtnCooling :: TheoryModel
nwtnCooling = tm nwtnCoolingRC
  [qw latentHeat, qw time, qw htTransCoeff, qw deltaT] ([] :: [ConceptChunk])
  [] [nwtnCoolingEqn] [] [makeCiteInfo incroperaEtAl2007 $ Page [8]]
  "nwtnCooling" nwtnCoolingNotes
Empty ---------------- c1 dq dfn
What kind of model is it: scalar equation 
JacquesCarette commented 4 years ago

Thanks. What we also really need is an answer to "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.

The analysis above is very close to the code. We need a more conceptual (pun intended) analysis that captures more what is 'intended' by each model, rather than merely list what is currently encoded.

muhammadaliog3 commented 4 years ago

This is what a naive solution would look like, by just removing what is never used.

data TheoryModel = TM { _con :: ConceptChunk , _vctx :: [TheoryModel] , _spc :: [SpaceDefn] , _quan :: [QuantityDict] , _ops :: [ConceptChunk] , _defq :: [QDefinition] , _invs :: [Relation] ~~ , _dfun :: [QDefinition]~~ , _ref :: [Reference] , lb :: ShortName , ra :: String , _notes :: [Sentence] } what operations are being defined by this theory? (_ops) what quantities are being defined by this theory? (_defq) (This is awfully similar to ""what quantities are being declared by this theory? (_quan)"") what (data) definitions are needed for this theory to make sense? (_dfun)

I was originally going to try and conceptually argue for the removal of these, but I could not find a clear conceptual problems with including them in theories. Then I began thinking are there any practical problems with these fields, that is why have no examples used them thusfar? Is it because Drasil examples are not complex/advanced enough for them to be used, is it that theories are not the appropiate place for new quanty_definition/dat_definitions/operations. I believe the answer is the first, that examples are not as complex yet.

JacquesCarette commented 4 years ago

Yes, the reason these are not used is that no example needs them, as of now.

Even though we'll eventually want to change TMs, this is unlikely the best place to start refactoring. The best place is likely to 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. [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.]

muhammadaliog3 commented 4 years ago

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.

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

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

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
                          }
JacquesCarette commented 4 years ago

@smiths you spent quite a bit of time figure out TM/GD/DD/IM -- where are your notes on this?

There is quite a bit of information (and code) that is very relevant to this in https://github.com/JacquesCarette/Drasil/issues/1373.

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'.

There is a lot of relevant information in #1373 and the code branch that it points to.

muhammadaliog3 commented 4 years ago

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.

JacquesCarette commented 4 years ago

Almost. I think it makes sense (and will be easier) for QDefinition itself to remain for single equations. You'll need new structures for the other cases. In more detail:

  1. yes to removing relationconcept, but we want to replace them with a new data-structure that describes different kinds of definitions
  2. yes to both. [I managed to do it in a branch]
  3. see above.

So other than defining a new data-structure instead of changing QDefinition, you had it right.

I'm going to warn you again: there are tricky spots. You will likely make a change (successfully!!) and then discover that the examples need to be tweaked to work properly, and that leads to another change, then another, and then things go sideways. The best thing to do is NOT to power through it! It is to see that what seemed like a simple change actually depends on something else being fixed first (sometimes, you have 2 or even 3 levels of that). Your best bet is to fix the "leaf" problem first (in another branch), then proceed. In as small pieces as possible. That is why my branch never got merged in, the 'rabbit hole' turned out to be a vast cavern.

muhammadaliog3 commented 4 years ago

So to be clear when classifying equations we should not change QDefinitions. The data structure for "equation type" should be created+determined elsewhere AFTER a given qdefinition has been created.

JacquesCarette commented 4 years ago

Yes to the first sentence. No to the second (if I understand you): you should define a new datastructure 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.

muhammadaliog3 commented 4 years ago

@JacquesCarette (Perhaps @smiths could answer this) Quick question on preference. We basically need a new data structure for classifying QDefinitions into 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!

I think a better way would be to define the following

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

Now ModelKinds can contain any combination of equationType. It is now easier to check if the equationType is a Differential (just check if the list contains Differential). Furthermore it becomes easier to check if an equation is NONdifferential (just check if the list does NOT contain Differential). This is an alternative to long pattern matches.

JacquesCarette commented 4 years ago

I quite agree that the naive way to do it does not scale. [BTW, you should check out how my name is actually spelled.]

What we'll want to do is to create a more general notion of 'definition' which does contain inside of it the information needed to know its "type".

Question: are two two lists supposed to be of the same length?

muhammadaliog3 commented 4 years ago

Question: are two two lists supposed to be of the same length?

No they don't. I think an example would help here. 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"]

JacquesCarette commented 4 years ago

I don't like that design. It is too imprecise. Differential should mean that all equations should be differential (but "a = g" isn't). And you shouldn't have 2 definitions of the same thing (such as a).

The 'direction' of the design is good, the details need revisited.

smiths commented 4 years ago

I agree with @JacquesCarette about having too imprecise a design. I'm not sure the combinatorial explosion of cases is necessarily that bad, at least if we can define a default and then the variations from it. Most equations will be scalar, nondifferential, singular, equational and real. We will occasionally have a deviation from this, but the defaults will often not change. I don't know if it is too different from what we are now discussing, but the default behaviour option is what @bmaclach used for his design for setting generation variabilities. Every project has default variabilities. We only have to explicitly set those that vary from the default.

There is a good chance that I don't understand well enough how we are using the QDefinition classifications, so my comment above might not be relevant. :-)

smiths commented 4 years ago

Above (https://github.com/JacquesCarette/Drasil/issues/1601#issuecomment-656807206) @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 commented 4 years ago

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.

  1. 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 image

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

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

  1. 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 commented 4 years ago

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:

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 commented 4 years ago

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.

  1. 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 commented 4 years ago
  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).

  1. 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 commented 4 years ago

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.

image image image image image image

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 commented 4 years ago

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

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"]

smiths commented 4 years ago

Thank you for the summary @muhammadaliog3. Very helpful!

JacquesCarette commented 4 years ago

Yes, both summaries are excellent.

muhammadaliog3 commented 4 years ago

@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 commented 1 year ago

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 commented 1 year ago

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