Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move Expr's Deriv into DisplayExpr #2628

Closed
balacij opened this issue Jun 25, 2021 · 13 comments · Fixed by #2791
Closed

Move Expr's Deriv into DisplayExpr #2628

balacij opened this issue Jun 25, 2021 · 13 comments · Fixed by #2791
Assignees

Comments

@balacij
Copy link
Collaborator

balacij commented Jun 25, 2021

We might need to convert DisplayExpr from the existing style of wrapping things into a 1-1 clone of Expr.

@balacij balacij self-assigned this Jun 25, 2021
@balacij
Copy link
Collaborator Author

balacij commented Jul 6, 2021

Started work on this, and I'm noticing that DisplayExpr is really just higher order version of Expr + defines.

@JacquesCarette
Copy link
Owner

Wrapper to. Or strict super-set. And it might indeed have 2 extra parts, new expressions and defines.

@balacij
Copy link
Collaborator Author

balacij commented Jul 7, 2021

I just wanted to give a quick update about this ticket. Moving Deriv out of Expr has ended up requiring a few other large changes too.

  1. Our EquationalModels currently contain QDefinitions (which contain Exprs) and are used for both InstanceModels and TheoryModels. With InstanceModels, we stick to generally "computable" things (however, in the examples that don't generate code, we have things that aren't yet computable). However, with TheoryModels, we need all functionality of the original Expr. So, we need to create a new ModelKind and a new version of QDefinition that carries DisplayExprs (a name that I think we'll change soon, but I'll leave for now). I will give this new ModelKind + QDefinition placeholder names until we have better names, but this might also be where we decide that it's time to split ModelKind into computable-ModelKinds and theoretical-ModelKinds so that TheoryModels & GenDefns contain the theoretical-ModelKinds but the DataDefinitions and InstanceModels are only allowed to carry the computable-ModelKinds. I'm not yet sure about the MultiDefn model, but I suspect that those will also need to be converted into using DisplayExprs instead of just Exprs for their internally held list of DefiningExprs.
  2. With ticket Remove as many RelationConcepts from the instance models as possible, by using ModelKind more #2371, we cleared up a lot of RelationConcepts (converting into EquationalModels) and moved a lot of the derivatives from the (a $= dy/dx... $= ... $= ...) Exprs into the derivations, but we still have a few stragglers that need to be fixed too.

Hopefully with this large change, it will be easier to move the integration and continuous intervals into DisplayExpr.

@JacquesCarette
Copy link
Owner

Adding @cd155 to the discussion.

My thought was that most differential equations would end up in DEModel, and that it could use a new type (not RelationConcept) as it does now.

But I guess that the issue is that we define some quantities by using derivatives? i.e. acceleration as derivative of velocity?

We really do want that in our expressions, and not just for display. Maybe we need ModelExpr to sit 'above' Expr, and that's where derivatives would live?

The other possibility is to move from recursive representations (like Expr) to functor representations (ExprF e) with Expr defined as Fix ExprF. That should let us be more flexible in our languages. Look up "Data Types a la Carte".

@balacij
Copy link
Collaborator Author

balacij commented Jul 7, 2021

Adding @cd155 to the discussion.

My thought was that most differential equations would end up in DEModel, and that it could use a new type (not RelationConcept) as it does now.

Great idea! That's a good connection I overlooked. The majority of the non-function-related RelationConcepts that contained a sy X $= ... were already converted into EquationalModels. Since the DEModels aren't 'directly' computable at the moment, we will also need to convert RelationConcepts to also use the DisplayExpr/ModelExpr. I think the ODE information packets for code generation should still use the CodeExprs directly that we have, and later see how if we can translate these ModelExprs into the related CodeExprs, or if we need to create extra classifications.

But I guess that the issue is that we define some quantities by using derivatives? i.e. acceleration as derivative of velocity?

Yes, for the ones that were of the form sy X $= ... specifically, I converted them into EquationalModels. The DEModels were left for the things that were expressed as a relation. I think this is still ok/good because we get to keep that information in the code, so as long as we convert (which is what I planned to do) the EquationalModels that contain a ModelExpr/DisplayExpr into a new ModelKind (named DEqModel for the time being, for "Display Equational Model", but this should be changed).

We really do want that in our expressions, and not just for display. Maybe we need ModelExpr to sit 'above' Expr, and that's where derivatives would live?

Yes! I agree. I think that we will also need to push the Defines component of DisplayExpr/ModelExpr out of it too, but that could be done a bit later I think.

The other possibility is to move from recursive representations (like Expr) to functor representations (ExprF e) with Expr defined as Fix ExprF. That should let us be more flexible in our languages. Look up "Data Types a la Carte".

Thanks, I will read this paper. I will follow up here after.

@balacij
Copy link
Collaborator Author

balacij commented Jul 7, 2021

This ticket will need to be split up into multiple PRs so that it's not too ridiculous to review. Approximately,

@balacij
Copy link
Collaborator Author

balacij commented Jul 7, 2021

We have some DataDefinitions that currently contain Derivs and I'm trying to figure out whether or not this should be allowed (because DataDefinitions are supposed to be QDefinition carriers, and we're going to need to split QDefinitions into 2 kinds of QDefinitions -- one for Expr and one for ModelExpr). I thought that they (Derivs) shouldn't be allowed in DataDefinitions because DataDefinitions are very simple information packets (directly "observable"), but re-reading the discussion from #2599, I don't think we explicitly mentioned anything about this really. Should DataDefinitions allow for either kind of QDefinition? Should DataDefinitions only allow for directly observable expressions/QDefinitions? If so, I imagine we would want to convert most of the DataDefinitions that currently contain derivatives into GenDefns.

@JacquesCarette
Copy link
Owner

We want to maximize re-usability, which for the new organization means using Expr over ModelExpr for example. Deriv is a very important concept at the specification level, and should be regarded as "well understood". We definitely need to allow it in as many places as possible, including in right hand sides of definitions.

@balacij
Copy link
Collaborator Author

balacij commented Jul 13, 2021

Small update after today's meeting:

@smiths brought up some great points that I believed cleared up some things for me here.

  1. I had misunderstood DataDefinitions. I thought that DataDefinitions should be used in code generation, but from what @smiths mentioned, they shouldn't -- they are definitions, and only InstanceModels should be used for code generation.
  2. Deriv might be something that we should keep in Expr, however, we might still want to have Deriv taken out for the first pass of typing and add it back later (when we decide on how we want to implement it).

Regarding (1), projectile and pdController both already don't require DataDefinitions for code generation, but it appears that GlassBR does. Removing all usage of the _datadefs param of SystemInformation in the codeSpec function (converts SIs into CodeSpecs results in the following error:

cd "build/GlassBR" && stack exec -- "glassbr" 
glassbr: The following outputs cannot be computed: isSafePb, isSafeLR, probBr, stressDistFac
Unused definitions are: isSafePb, isSafeLR
Known values are: plateLen, plateWidth, charWeight, pbTol, tNT, glassTy, nomThick, sdx, sdy, sdz, sflawParamM, sflawParamK, modElas, loadDur, lShareFac, dimMax, dimMin, arMax, cWeightMax, cWeightMin, sdMax, sdMin, stressDistFacMin, stressDistFacMax
CallStack (from HasCallStack):
  error, called at ./Language/Drasil/CodeSpec.hs:173:20 in drasil-code-0.1.9.0-744zRuqLmwrBswCFNNjRg3:Language.Drasil.CodeSpec
make: *** [Makefile:158: glassbr_gen] Error 1

Should we still make DataDefinitions use a new version of QDefinitions that use ModelExpr/DisplayExprs instead of Exprs? I'm not so sure anymore, but I think it would be the safest option.

@smiths
Copy link
Collaborator

smiths commented Jul 16, 2021

@balacij thank you for the summary of our meeting discussion and the material you have extrapolated from the discussion.

You are correct that I said that DataDefinitions aren't needed in code generation, but as we continued the discussion, I did think of some examples where we might use them. I think there are many cases where the DataDefinitions aren't directly part of the generated code, but my initial statement was too simplistic.

The example we discussed was for a simple rigid body motion problem. For this example, we can think of the problem in 1D. We have the following theory:

T1. F = ma

Associated with this, we have the data definitions:

D1. a = dv/dt
D2. v = ds/dt

From this information, we find a refined theory model, what we have been calling the instance model:

T2. d^2s/dt^2 = F/m, together with initial conditions

We then have requirements:

R1. Input F, m, the initial position and the initial velocity
R2. Solve the T2 to find s
R3. Output s.

The requirement actually tell us what code we need to generate -- code to collect the inputs, code to solve the ODE and code to output the results.

This is why I suggested that we only need to worry about instance model for code generation. However, as we discussed further, I realized there could be another requirement:

R4. Output v

To calculate v we need D2, so data definitions do sometimes turn into code.

I'm sure as we think further about it, we will see further examples.

I think GlassBR also has examples that turn into code. I think some of the data definitions become code. For GlassBR we could probably recharacterize those definitions as theories.

What we need to do is really solidify what we mean by theory and definition. I'd like to add to that that we should understand requirements and the connection between the SRS pieces and generated code.

@balacij
Copy link
Collaborator Author

balacij commented Jul 16, 2021

@smiths My apologies for the misunderstanding. I think I will need to spend a bit of time going through GlassBR's DDs and understand how this is handled. Thank you for the clarification!

@smiths
Copy link
Collaborator

smiths commented Jul 17, 2021

@balacij there is nothing to apologize for. I did say what you remembered hearing, but I changed my mind. 😄 Our understanding on this topic is going to continue to evolve.

@JacquesCarette
Copy link
Owner

In many ways, there is very little difference between a "data definition" and a "quantity definition" (i.e. type QDefinition). The main difference is that one is used inside theories (quantity definitions) while the other "extends" a theory. But they are kind of the same thing otherwise.

So the first thing to do would be to look at the "payload" of both of these things, i.e. all the fields (recursively) of both. We should then make sure that the fields they have in common mean the same thing, and then explain the differences in the other fields. That will let us know how to move forward. There will still be some sort of difference between them, but it might be slight.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
3 participants