Many-Sorted Algebraic Semantics for Dimensional Quantity Calculus
- 1Department of Electrical and Electronic Engineering, Shizuoka University, 3-5-1 Johoku, Chuo-ku, Hamamatsu 432-8561, Japan
Abstract
We study polynomial expressions with physical dimensions and the effect of setting an invertible reference quantity equal to one. Dimensions are treated as sorts indexed by a finitely generated free Abelian group D. Using standard categorical constructions, we describe the free D-graded commutative real algebra and its induced finitary monad TD. Monad multiplication is homogeneous polynomial substitution. We identify its Eilenberg–Moore category with the category of D-graded commutative real algebras and give a D-sorted Lawvere theory for the same structure. We then distinguish normalization, coarsening of degree labels, and specialization u=1. For an invertible homogeneous reference u of infinite-order degree g, the specialization map A⟶A/(u−1), with the quotient graded by D/Zg, is injective on each original homogeneous component. Thus, two expressions of the same original degree are equal if and only if their images after specialization are equal, although mixed-degree information may be lost. An equation-of-motion example illustrates dimensional typing, the imposition of a physical relation, and reference specialization. For finitely presented models, the real Nullstellensatz yields existence and joint equation-detection criteria for surjective graded numerical presentations. Models with the same full degree support and real radical relations can differ in both properties. A corollary gives finite algebraic certificates for validity in all such presentations.
Related
- An Algebraic Foundation of Rate-Product Style Quantity Calculus
- A Chain- and Diagram-Level Semantics for Morphological Calculus Refinement, monodromy, and bivector orbit decompositions
- Modal weak Kleene logics: algebraic semantics and Jónsson-Tarski representation
- Tense Logic via Truth Degrees: An Algebraic Completeness Result for Kashima's Calculus
- Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4
BibTeX
@article{yaji2026manysorted,
title = {{Many-Sorted Algebraic Semantics for Dimensional Quantity Calculus}},
author = {Kohei Yaji},
journal = {Mathematics},
year = {2026},
month = nov,
doi = {10.3390/math14224128},
url = {https://www.mdpi.com/2227-7390/14/22/4128},
note = {CC BY 4.0},
}
RIS
TY - JOUR
TI - Many-Sorted Algebraic Semantics for Dimensional Quantity Calculus
AU - Kohei Yaji
PY - 2026
DA - 2026/11/10
JO - Mathematics
DO - 10.3390/math14224128
UR - https://www.mdpi.com/2227-7390/14/22/4128
AB - We study polynomial expressions with physical dimensions and the effect of setting an invertible reference quantity equal to one. Dimensions are treated as sorts indexed by a finitely generated free Abelian group D. Using standard categorical constructions, we describe the free D-graded commutative real algebra and its induced finitary monad TD. Monad multiplication is homogeneous polynomial substitution. We identify its Eilenberg–Moore category with the category of D-graded commutative real algebras and give a D-sorted Lawvere theory for the same structure. We then distinguish normalization, coarsening of degree labels, and specialization u=1. For an invertible homogeneous reference u of infinite-order degree g, the specialization map A⟶A/(u−1), with the quotient graded by D/Zg, is injective on each original homogeneous component. Thus, two expressions of the same original degree are equal if and only if their images after specialization are equal, although mixed-degree information may be lost. An equation-of-motion example illustrates dimensional typing, the imposition of a physical relation, and reference specialization. For finitely presented models, the real Nullstellensatz yields existence and joint equation-detection criteria for surjective graded numerical presentations. Models with the same full degree support and real radical relations can differ in both properties. A corollary gives finite algebraic certificates for validity in all such presentations.
SN - 2227-7390
ER -