Extending the Data Type of Common Meadows: the Case of Specifying Entropy

Numerical computation rests on the addition, subtraction, multiplication and division of real numbers. Data types with these operations can be analysed algebraically and logically by the theory of common meadows: a common meadow is an enrichment of a field with a partial division operation that is made total by assuming that division by zero takes a default value ⊥ adjoined to the field. Common meadows have an equational axiomatisation that supports key algebraic laws for calculation and reasoning. We discuss defining other partial functions on numerical data types based on common meadows. As a case study, we explore methods to define entropy and other information measures. To a common meadow of real numbers we add a binary logarithm log2(−) that we assume to be total with log2(p)=⊥ for p ≤ 0. With log2 and other auxiliary operations, such as a left-biased multiplication ∘ ×  and sign function s(−), we form data types to define entropy measures for all inputs by formulae that are simple terms built from the operations of the data types, and without ‘conventions’ to avoid partiality.