A heretical view on type embedding

Publisher Website
Google Scholar
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.

This publication has 0 references indexed in Scilit: