NoPCM Case Study: Fix Conservation of Thermal Energy Theory (Discussion)

[smiths]

As a step toward the refined theories version of NoPCM, we should discuss updating the conservation of thermal energy theory.

The conservation of thermal energy theory in NoPCM (and in SWHS) should probably be updated to explicitly show the dependence of each variable on the relevant independent variables. In the current version of NoPCM, TM:consThermE should be updated to fix the Equation (to show the dependence on spatial position, time and temperature), Description (to define the spatial position (the vector x)) and Notes (to add the description of the dependencies and make explicit that the form of the equation is coordinate system independent) field to match the following:

@balacij, can you estimate how much work would be required to do this update?

@JacquesCarette, we should decide whether it is worthwhile to update the NoPCM document to reflect the changes mentioned above soonish, or whether we should instead wait until we have discussed the refined theories version of our SRS further first. The changes are related, but they are independent. We don't actually need refined theories to add more explicit assumptions to the NoPCM (and SWHS) examples. However, the additional details do become more difficult to handle manually in writing a manual document, and my guess is they will currently involve "fiddely" work to add them within Drasil.

[balacij]

This theory is imported from SWHS. Would you want these changes to also affect SWHS? If we do, it might just add a bit of extra time spent working to adjust SWHS as well.

I think x is a new variable, but creating it shouldn't be difficult at all.

The "Description" is automatically generated using the variables found in "Equation" section, so that part should be done for us automatically once the equation shows x in the function application.

The "Notes" section appears to be a matter of formatting, which shouldn't take much time (unless we want to be really strict on ourselves and make sure that we're fully using all the Sentence combinators available).

Regarding the "Equation" section, q, g, ρ, C, and T are currently typed as Reals (their Space is Real), so I think we would need to convert their types into functions as required, and add function applications to the equation. To be clear, would the T provided as an input to ρ and C also show its arguments as well, or are we passing the function T to ρ and C? Additionally, with editing the types of the variables, there might also be some inconsistencies in the rest of the document that would need to be fixed, but I think you covered the majority in the updated pdf. A few areas might require a bit of special attention. For example, the current NoPCM defines ΔT(t) as T(t)−Tenv(t) in TM:nwtnCooling (the T here is currently inconsistent with the Space/type of T), the T would need an extra parameter, and we might reconsider the description/definition of ΔT.

Ultimately, I don't think it would be difficult to make these specific changes (mainly because it looks like it's already thought through completely in the manually updated pdf), but the surrounding areas might take some time and care to make sure it's consistent with the pdf/changes.

[smiths]

Thank you for the info @balacij. Very helpful as always!

Yes, I would want the theory for the conservation of thermal energy to also be updated for SWHS. We want our theories, especially the most general theories, to be reusable. If they aren't, then we've made a mistake. :smile: Hopefully updating (fixing) the general theory in one place, will fix it everywhere it occurs, without much (any?) extra work.

Yes, x is a new variable. We implicitly ignored space in the first version because for SWHS and noPCM we don't actually need to worry about space. Since the tank is well-mixed, there is no variation in temperature, or thermal properties, between each location in space. For other thermal problems, we won't be able to make this same assumption. Related to the point about reuse above, the current version of the conservation of thermal energy is not as reusable as we would like it to be. Our current conservation of thermal energy theory isn't as general as it could be (because it doesn't mention space), and even worse, it doesn't explicitly mention the assumption that is being made about spatial variation.

For the "Notes" section update, I'm fine with not using all of the sentence combinators. That is something that we can emphasize more over time, if it proves to be useful. I would like any symbols that appear in the Notes to automatically match the symbols used in the rest of the document, without the need to enter them manually in the Notes. For instance, I wouldn't want us to say $\rho$ in a Sentence. I would want us to indicate that we want the symbol for the concept of density. (I'm pretty sure that is a straightforward thing to do in Drasil.)

The point about the types of q, g etc being Real is a good one. We'll have to think what to do about that. At the level of the conservation of thermal energy theory C (for instance) is a function: Vector X Real -> Real, but by the time we get to the final theories (currently instance models), C is a Real. (I put Vector in there because x is a spatial location, which is represented by a vector in space.) We made simplifying assumptions to make C a constant that doesn't depend on space or temperature. We never make any use of the function for C. We know that C is a function, but we never need to define the function. This is similar to how we are aiming to handle interpolation. We postpone providing the details of how to do interpolation. For C, in this particular problem, we never actually have to define the function. (I don't know if it is the same thing, but it reminds me of lazy evaluation.)

I understand your confusion about $T$. It is a dependent variable in one part of the equation and an independent variable in another. In general thermal problems are coupled. The equation to find temperature depends on temperature, because the thermal properties change with temperature. The type of C is Vector X Real -> Real, even though temperature is itself a function. When we evaluate C we can assume that we know the temperature. The type of temperature is Vector X Real -> Real. (We don't combine these to say that the type of C is Vector X (Vector X Real -> Real) -> Real.)

You have a good point about the changes to the conservation equation having a ripple effect. The current version of Newton's Law of Cooling would be effected. I actually no longer like that the Newton's Law of Cooling introduces DeltaT. I guess if we make changes to the Conservation theory, we'll have to also edit Newton's law to follow the revised document.

The motivation for my question is that I think we will want at least two stages to any revision that heads us towards a "refined theories" version of noPCM (and SWHS). The first pass would be to fix the inconsistencies in NoPCM that I noticed while trying to add theories. The updates that are discussed in this issue are examples of those inconsistencies (like not mentioning the spatial variation when we really should have.) The second pass would be to actually change how we represent theories to more explicitly take advantage of the concept of refinement.