Types, equations, dimensions and the Pi theorem

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Botta, Nicola, Jansson, Patrik
Format: Preprint
Published: 2023
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914400251674624
author Botta, Nicola
Jansson, Patrik
author_facet Botta, Nicola
Jansson, Patrik
contents The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to formalize basic notions of dimensional analysis: those of dimension function, physical quantity, homomorphic measurement, the covariance principle and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.
format Preprint
id arxiv_https___arxiv_org_abs_2308_09481
institution arXiv
publishDate 2023
record_format arxiv
spellingShingle Types, equations, dimensions and the Pi theorem
Botta, Nicola
Jansson, Patrik
Programming Languages
Logic in Computer Science
The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to formalize basic notions of dimensional analysis: those of dimension function, physical quantity, homomorphic measurement, the covariance principle and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.
title Types, equations, dimensions and the Pi theorem
topic Programming Languages
Logic in Computer Science
url https://arxiv.org/abs/2308.09481