A heretical view on type embedding

ABSTRACT

Based on a useful concept of type-ordering that implicity or explicitly underlies the type of certain programming languages, it is shown that the type "boolean" can be viewed as a subtype of the type "natural" and hence, by transitivity, of "integer", "rational", and so on. This implies defining 𝔹 = {0, 1 } rather than B = {false, true}, and results in many useful mathematical properties that are not available with the latter definition. It is shown how the danger of confusion (which is often considerably overrated anyway) can be eliminated, and how a slight modification in the formulation of predicate logic can accommodate this definition rather conveniently. The theoretical and practical advantages are illustrated by means of examples.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages