remove the use of 'p' and 'v'

[janim2-2004]

As mentioned in #3189 we would like to stop using p (position) and v (speed) instead use p(t) and v(t) respectively.

these, along with other uses of p and v should be changed to be dependent on time.

[janim2-2004]

Looking into this more I realize it should be done through a more fundamental change of how we handle units. There is simply to may variables that are very close to each other in meaning. We could implement a hardcoded solution, but this should probably wait until we finish with our analysis of space, symbol and unit.

[smiths]

I'm not sure I understand your point @ManvendraJani. The units for p and p(t) are the same. The units for v and v(t) are the same. The analysis of units won't change anything. Eventually we want to change how we handle functions, so that p(t) is more meaningful than it is right now. For the moment though, I think it is still worthwhile to remove instances of p and v, since in both cases where the symbols are used, the meaning is p(t) and v(t).

[janim2-2004]

The issue is that although the units are the same the meaning is different. Currently, v (speed) represents the magnitude of the velocity while v(t) (linear velocity) represents the velocity in a given direction. We are trying to represent both using the same units, and currently we cant do that. This falls into a similar vein as the discussion in #3432.

[smiths]

Yes, we can represent them with the same units. The units for a vector are the units for each component of the vector. (This is a convention that we could probably more clearly communicate in the documentation.) No matter the outcome of our discussion on units, speed will have units of m/s and the components of the velocity vector will have units of m/s.

I think we can proceed with fixing p(t) and v(t) without worrying about units. In the future we will improve Projectile even further, but the move to p(t) and v(t) is a move in the right direction, even if the implementation isn't as elegant as it will eventually be. 😄

[janim2-2004]

I am sorry I was using the wrong term, I meant they have the same symbol.
For example, when representing linear velocity and speed, on paper we would say v(t) for both and that is fine. However, Drasil does not allow us to say that, we cannot have 2 different concepts with the same symbol.

So, besides making much larger design changes the only solution is to mark all magnitudes of velocity(speed) as linear velocity and then manually change wherever we use the other characteristics of speed (like the Noun Phrase and definition) to match what we want to say.

I was saying that we should wait until after the discussion on space, symbol and units as we would not want to make a big change right before we might completely change how we use them.

[smiths]

@ManvendraJani can you tell me the concept that we attach to v and the concept that we attach to v(t). I'm not convinced that whatever distinction is being made isn't artificial. I'm heading to a meeting right now, so I don't have time to look at the SRS. 😄

[janim2-2004]

This is how the UnitalChunk defines these.
The UnitalChunk itself is formed by adding the symbol and unit from the ConceptChunk, which is a description with a 'name'.

[JacquesCarette]

Drasil does not allow us to say that, we cannot have 2 different concepts with the same symbol.

Can you point out the code that disallows that? It is definitely "in bad taste" to use the same symbol for two different things however, I'm not sure it is legitimate to not allow it at all. [Same UID is a different thing, that is definitely not allowed.]

My guess is that the doubling of concepts in the above chart might be a hack because older Drasil simply couldn't do certain things. What it says is not wrong, but also it's not clear that that's what we actually want to use in practice.

[smiths]

@ManvendraJani I've looked at Projectile more closely and there are some inconsistencies in the spec. For instance, speed is a poor name for the magnitude of the velocity vector because magnitude is always positive, but in some cases speed is negative to show that it is going in the opposite direction. The magnitude of the velocity vector can change over time, but calling it v(t) is confusing because we use v(t) for 1D velocity. The magnitude is 1D (scalar), but it is associated with a 2D vector. We could write || v(t)||, but this would likely make the document confusing.

I now agree that we should wait to figure out the best way to present this information in Projectile, but we aren't so much waiting for the discussion of symbol and state. What we really need to do is think about the refined theories version of Projectile. The issues come up when we combine knowledge of vectors with knowledge of physics. We've combined them in a somewhat ad hoc way at the moment. I don't think we need a fully formal treatment, but we do need to be more rigorous.

[janim2-2004]

Can you point out the code that disallows that?

https://github.com/JacquesCarette/Drasil/blob/2fa75082389442d317e0c63ad92d9d3879121a33/code/drasil-docLang/lib/Drasil/Sections/TableOfSymbols.hs#L22C1-L44C1

This change was made regarding this PR.

[janim2-2004]

Can you point out the code that disallows that?

https://github.com/JacquesCarette/Drasil/blob/2fa75082389442d317e0c63ad92d9d3879121a33/code/drasil-docLang/lib/Drasil/Sections/TableOfSymbols.hs#L22C1-L44C1

This change was made regarding this PR.

I realize the link does not show the code

[JacquesCarette]

So you are somewhat misinterpreting what's going on. It's not that Drasil disallows duplication of symbols, it is that in the context of an SRS about a single piece of software, then symbols should be unique. It is a kind of "local uniqueness" but not global uniqueness.

[balacij]

Surprisingly complicated! Assuming that $v$ is not just a constant copy of $v(t)$, then this post is relevant. Otherwise, please disregard.

Seeing $v = \frac{dp}{dt}$ is interesting because it implies that $t$ is potentially (hopefully 'likely') used in $p$'s definition and in $v$'s (or, $v(t)$'s rather), and that $v$ is a function of $\mathbb{R}^+$. The assumption that $v$ is a function is fair because its symbol declaration carries type information. However, is it fair to connote $t$ as the argument/variable used in whatever formula we use to define $v$, $v(t)$? Obviously, it's fair for us and very conventional, but for Drasil, it pops out of nowhere/meaningless. If we were to ask Drasil to check that this expression were well-typed and sane (these are ModelExprs, so they're not guaranteed!), we would probably want it to check that $t$ is a variable used in the declaration of $v$ at least. But do we always want to have a well-defined declaration, computable formula for $v$? Probably not. I imagine we would want to assume variables are calculable without known formulas.

So, now the big question is: when is $t$ associated with $v$?

Some questions that might help us (or at least me) understand how to proceed:

• (context: defining $v$ [which is in a vacuum/globally]) Is it when we declare its type signature as being a function of $\mathit{Time}$ (an alias of $\mathbb{R}^+$ associated with dummy variable $t$ or $t_n$ for all $n \ge 0$)?
• Should we instead not be defining $v$ in a vacuum? Should $v$ be declared as something associated to $p$, and $p$ be defined as something associated with a formula that uses $t$ in its definition? In other words, should the symbol definition be moved to a theory definition, where we have formula declarations and could build "function parameter argument symbol associations"? This might mean that when we refer to a symbol like $v$ and desire association to $t$ (and of course, printing in an 'Engineering/Conventional' pretty-printing mode), we would need to refer to the formula that defines $v$. However, as I already explained my bias here -- we don't want to assume formulas exist, so we might need the ability to create "undefined formulas" or something of the likes that only serve the purpose of declaring association of function parameters with argument symbols.

(The issue of how and when $f$ or $f(...)$ should be used has been an issue for quite a while, so might as well try to understand it better.)

[EDIT: As already mentioned elsewhere, Drasil knows little about functions, but I think this is a good segue to teaching Drasil about functions]

[smiths]

I think part of the way out of our confusion is to attach type information to every symbol. We also want to avoid sloppy conventions that engineers and scientists (including me!) often use. In the refined theories version of projectile I tried to add type information to the symbols. In 1D, the type of v is a function type (t -> R). The type of v(t) is R. In the new version of projectile I also tried to remove the confusion around the magnitude of a vector versus the component of a 1D vector. That is why I explicitly added the magnitude angle representation (polar representation) of a vector as a theory. Although it is still in the table of symbols, I don't think we still have the problem of v meaning speed and v(t) meaning 1D speed. I use |v| for magnitude, and v is the function mentioned above and v(t) is the speed at time t. (Similar changes are made for position.)

If we can get the new version of projectile into Drasil, I think we'll really start to see the value of Drasil. Manually creating a document with all this information consistently presented is too difficult for most humans. I think Drasil will also catch incompleteness in what I've done.

Another idea that we'll need to look at with respect to the clash of symbols, I don't think we'll be able to continue with one table of unique symbols for the entire document. For instance, velocity is 1D, 2D and 3D in the document for projectile. It is natural to use the same symbol for all 3, with the symbol being bold for the 2D and 3D cases, but the three have different types. At least to this point, the document seems to naturally have groups of theories that can share the same set of symbols.

[balacij]

I think part of the way out of our confusion is to attach type information to every symbol.

I believe we already have this, it's just not shown in the SRS artifacts. We just call it a 'space' on the backend (I suppose we should change that...):

Drasil/code/drasil-lang/lib/Language/Drasil/Chunk/DefinedQuantity.hs

Lines 23 to 32 in 061f90e

	-- | DefinedQuantityDict is the combination of a 'Concept' and a 'Quantity'.
	-- Contains a 'ConceptChunk', a 'Symbol' dependent on 'Stage', a 'Space', and maybe a 'UnitDefn'.
	-- Used when we want to assign a quantity to a concept. Includes the space, symbol, and units for that quantity.
	--
	-- Ex. A pendulum arm can be defined as a concept with a symbol (l), space (Real numbers), and units (cm, m, etc.).
	data DefinedQuantityDict = DQD { _con :: ConceptChunk
	, _symb :: Stage -> Symbol
	, _spa :: Space
	, _unit' :: Maybe UnitDefn
	}

Another idea that we'll need to look at with respect to the clash of symbols, I don't think we'll be able to continue with one table of unique symbols for the entire document.

I agree. I wonder what our criteria is for deciding which are relevant. Assuming all the problems we discuss are ICO-style, then we probably only want to show symbols immediately mentioned in the inputs and outputs, and those found in the data definitions and other calculation-related formulas. For libraries, we might not want a global table of symbols, or we might want to allow users to define one on their own rather, grouping whatever symbols they deem fit, until we can come up with a better criterion.

[JacquesCarette]

Furthermore I think we need to further dis-entangle display and meaning. It should be okay to elide the (t) in v(t) in many settings.

This will force us to make it clearer when we're talking about velocity as a function of time and an instantaneous velocity at a given time. They have different types! (Same with velocities in different dimensions).

We will still want to associate 'display hints' to quantities. Right now, we have 'display orders' (i.e. you WILL display things this way). And our display orders don't necessarily match the type of the associated quantity.