Physical quantities

Konrad Hinsen

Context quantities
uses builtins/real-numbers

1 Generic quantities

We define Q to represent any physical quantity, and Qnz ⊆ Q to represent the subset of non-zero quantities by which it is admissible to divide. The product and quotient of any two quantities is then again a quantity, with appropriate special cases for quantities that can be proven to be non-zero:

Q × Q : Qℝ
Qnz × Qnz : Qℝnz
Q ÷ Qnz : Qℝ
Qnz ÷ Qnz : Qℝnz

The result sort of these operators is not Q but Qℝ or Qℝnz ⊆ Qℝ, because in the special case of a quotient of same-kind quantities, the result is a pure number. We therefore define

Q ⊆ Qℝ
Qnz ⊆ Qℝnz
ℝ ⊆ Qℝ
ℝnz ⊆ Qℝnz

We can also multiply or divide quantities by numbers:

ℝ × Q : Q
ℝnz × Qnz : Qnz
Q ÷ ℝnz : Q
Qnz ÷ ℝnz : Qnz

The simplification strategy is to reduce quantities to the form f × q, with q a non-reducible quantity, wherever possible.

Combine multiple numerical prefactors into one:

f1 × (f2 × q) ⇒ f1 × f2 × q
  ∀ f1 : ℝ
  ∀ q : Q
  ∀ f2 : ℝ
f1 × ((f2 × q1) ÷ q2) ⇒ f1 × f2 × (q1 ÷ q2)
  ∀ q2 : Q
  ∀ q1 : Q
  ∀ f1 : ℝ
  ∀ f2 : ℝ

Replace division by multiplication:

q ÷ f ⇒ (1 ÷ f) × q  ∀ f : ℝnz  ∀ q : Q
q1 ÷ (f × q2) ⇒ (1 ÷ f) × (q1 ÷ q2)
  ∀ q1 : Q
  ∀ q2 : Qnz
  ∀ f : ℝnz

Remove quantities of zero magnitude from sums:

q1 + (0 × q2) ⇒ q1  ∀ q2 : Q  ∀ q1 : Q
q1 - (0 × q2) ⇒ q1  ∀ q2 : Q  ∀ q1 : Q
(0 × q2) + q1 ⇒ q1  ∀ q2 : Q  ∀ q1 : Q
(0 × q2) - q1 ⇒ q1  ∀ q2 : Q  ∀ q1 : Q

Context template
extends quantities

2 A template for specific quantities

The definitions and rules for specific quantities such as mass or time are essentially the same. We define a template for a fictitious quantity SQ ⊆ Q with SQnz ⊆ Qnz and SQnz ⊆ SQ, and derive the real physical quantities by name substitution.

The sum and difference of two same-kind quantities is again a quantity of the same kind:

SQ + SQ : SQ
SQ - SQ : SQ

Multiplication and division by numbers also yields same-kind quantities:

ℝ × SQ : SQ
ℝnz × SQnz : SQnz
-(SQ) : SQ
SQ ÷ SQnz : ℝ
SQnz ÷ SQnz : ℝnz
SQ ÷ ℝnz : SQ
SQnz ÷ ℝnz : SQnz

Finally, same-kind quantities can be compared:

SQ < SQ : boolean
SQ > SQ : boolean
SQ ≤ SQ : boolean
SQ ≥ SQ : boolean

In the simplification rules, we use the variables sq:SQ, sq1:SQ, sq2:SQ and f:ℝ, f1:ℝ, f2:ℝ.

Combine sums and differences of the same SQ with different numerical prefactors:

(f1 × sq) + (f2 × sq) ⇒ (f1 + f2) × sq
(f1 × sq) - (f2 × sq) ⇒ (f1 - f2) × sq

Reduce quotients of two SQs to a number:

sq1 ÷ (f × sq2) ⇒ sq1 ÷ f ÷ sq2
(f × sq1) ÷ sq2 ⇒ f × (sq1 ÷ sq2)
sq ÷ sq ⇒ 1

Context template-test
extends template

2.1 Tests

Given two quantities a : SQ and b : SQ whose quotient we define as b ÷ a ⇒ 10, we can test the simplification rules:

2 × (3 × a) ⇒ 6 × a ✓
2 × (a ÷ 3) ⇒ 2/3 × a ✓
(2 × a) ÷ (3 × a) ⇒ 2/3 ✓
(2 × b) ÷ (3 × a) ⇒ 20/3 ✓
(2 × a) + (3 × a) ⇒ 5 × a ✓
(2 × a) - (3 × a) ⇒ -1 × a ✓

Context mass
includes transformed template

3 Mass

Replace SQ by M and SQnz by Mnz in the template:

Sorts: ℝ, boolean, Mnz, Q, Qnz, M, ℝnz
Subsort relations: Mnz ⊆ Qnz, M ⊆ Q, Mnz ⊆ M
Operators:

-(M) : M
ℝnz × Mnz : Mnz
ℝ × M : M
Mnz ÷ Mnz : ℝnz
M ≥ M : boolean
M > M : boolean
Mnz ÷ ℝnz : Mnz
M - M : M
M ≤ M : boolean
M + M : M
M ÷ ℝnz : M
M ÷ Mnz : ℝ
M < M : boolean

Rules:

(f1 × sq) + (f2 × sq) ⇒ (f1 + f2) × sq
  ∀ sq:M
  ∀ sq2:M
  ∀ sq1:M
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
(f1 × sq) - (f2 × sq) ⇒ (f1 - f2) × sq
  ∀ sq:M
  ∀ sq2:M
  ∀ sq1:M
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
sq1 ÷ (f × sq2) ⇒ sq1 ÷ f ÷ sq2
  ∀ sq:M
  ∀ sq2:M
  ∀ sq1:M
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
(f × sq1) ÷ sq2 ⇒ f × (sq1 ÷ sq2)
  ∀ sq:M
  ∀ sq2:M
  ∀ sq1:M
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
sq ÷ sq ⇒ 1
  ∀ sq:M
  ∀ sq2:M
  ∀ sq1:M
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ

Assets:

Context length
includes transformed template

4 Length

Replace SQ by L and SQnz by Lnz in the template:

Sorts: ℝ, boolean, Lnz, Q, Qnz, L, ℝnz
Subsort relations: Lnz ⊆ L, L ⊆ Q, Lnz ⊆ Qnz
Operators:

Lnz ÷ ℝnz : Lnz
L ≤ L : boolean
L + L : L
L ≥ L : boolean
L - L : L
-(L) : L
L < L : boolean
Lnz ÷ Lnz : ℝnz
L > L : boolean
ℝnz × Lnz : Lnz
ℝ × L : L
L ÷ Lnz : ℝ
L ÷ ℝnz : L

Rules:

(f1 × sq) + (f2 × sq) ⇒ (f1 + f2) × sq
  ∀ sq:L
  ∀ sq2:L
  ∀ sq1:L
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
(f1 × sq) - (f2 × sq) ⇒ (f1 - f2) × sq
  ∀ sq:L
  ∀ sq2:L
  ∀ sq1:L
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
sq1 ÷ (f × sq2) ⇒ sq1 ÷ f ÷ sq2
  ∀ sq:L
  ∀ sq2:L
  ∀ sq1:L
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
(f × sq1) ÷ sq2 ⇒ f × (sq1 ÷ sq2)
  ∀ sq:L
  ∀ sq2:L
  ∀ sq1:L
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ
sq ÷ sq ⇒ 1
  ∀ sq:L
  ∀ sq2:L
  ∀ sq1:L
  ∀ f:ℝ
  ∀ f1:ℝ
  ∀ f2:ℝ

Assets:

Context time
includes transformed template

5 Time

Replace SQ by T and SQnz by Tnz in the template (result now shown).

Context velocity
includes transformed template

6 Velocity

Replace SQ by V and SQnz by Vnz in the template (result not shown).

Context acceleration
includes transformed template

7 Acceleration

Replace SQ by A and SQnz by Anz in the template (result not shown).

Context force
includes transformed template

8 Force

Replace SQ by F and SQnz by Fnz in the template (result not shown).

Context angle
includes transformed template

angle π : angle

Context frequency
uses time
includes transformed template

frequency × T : ℝ frequency-nz × Tnz : ℝnz T × frequency : ℝ Tnz × frequency-nz : ℝnz

Context angular-frequency
uses time
uses angle
includes transformed template

angular-frequency × T : angle angular-frequency-nz × Tnz : angle-nz T × angular-frequency : angle Tnz × angular-frequency-nz : angle-nz

Context function-template
includes transformed template
includes transformed template

9 A template for functions from one quantity to another

This template defines functions from a domain quantity SQD to an image quantity SQI. The sort for such functions is SQD→SQI ⊆ Q→Q, function application is defined by SQD→SQI[SQD] : SQI.

It is convenient to provide some arithmetic:

Addition and subtraction of functions:
- f:SQD→SQI + g:SQD→SQI : SQD→SQI with
  (f + g)[x] ⇒ f[x] + g[x] ∀ x : SQD
- f:SQD→SQI - g:SQD→SQI : SQD→SQI with
  (f - g)[x] ⇒ f[x] - g[x] ∀ x : SQD
Addition and subtraction of constants:
- f:SQD→SQI + q:SQI : SQD→SQI with
  (f + q)[x] ⇒ f[x] + q ∀ x : SQD
- f:SQD→SQI - q:SQI : SQD→SQI with
  (f - q)[x] ⇒ f[x] + q ∀ x : SQD
- q:SQI + f:SQD→SQI : SQD→SQI with
  (q + f)[x] ⇒ q + f[x] ∀ x : SQD
- q:SQI - f:SQD→SQI : SQD→SQI with
  (q - f)[x] ⇒ q - f[x] ∀ x : SQD
Multiplication with scalars:
- s:ℝ × f:SQD→SQI : SQD→SQI with
  (s × f)[x] ⇒ s × f[x] ∀ x : SQD
- -(f:SQD→SQI) : SQD→SQI with
  -(f)[x] ⇒ -(f[x]) ∀ x : SQD

Context function-with-derivative-template
includes transformed function-template
includes transformed function-template

10 A template for functions with derivatives

The derivative of a function is given by 𝒟(SQD→SQI) : SQD→SQID, where SQID ⊆ Qℝ is the quotient of SQI and SQD.

It is a linear operator, i.e. for f:SQD→SQI, g:SQD→SQI, and s:ℝ we have

𝒟(f + g) ⇒ 𝒟(f) + 𝒟(g)
𝒟(f - g) ⇒ 𝒟(f) - 𝒟(g)
𝒟(s × f) ⇒ s × 𝒟(f)

Context function-with-finite-difference-template
includes transformed function-with-derivative-template

In numerical approximations, the derivative operator 𝒟(SQD→SQI) : SQD→SQID is replaced by the finite-difference operator Δ(f:SQD→SQI, h:SQDnz) : SQD→SQID. A finite-difference approximation is characterized by a parameter h:SQDnz, assumed to be a sufficiently small quantity.

Like the derivative operators, the finite-difference operator is linear, i.e. for two functions f:SQD→SQI and g:SQD→SQI, and a numerical scaling factor s:ℝ, we have

Δ(f + g, h) ⇒ Δ(f, h) + Δ(g, h)
Δ(f - g, h) ⇒ Δ(f, h) - Δ(g, h)
Δ(s × f, h) ⇒ s × Δ(f, h)

1	Generic quantities
2	A template for specific quantities
3	Mass
4	Length
5	Time
6	Velocity
7	Acceleration
8	Force
9	A template for functions from one quantity to another
10	A template for functions with derivatives