5  Theoretical aspects

We would like to point out here that there is a strong relation between type systems and logic. More precisely, the so-called Curry-Howard correspondence²³ relates types with propositions, and programs with proofs. It can be shown that type inference rules for the typed lambda calculus (i.e. functional programs) relate to natural deduction²⁴ in propositional logic. While this is traditionally presented for implication introduction and elimination (type inference rules for function abstraction and application) only, it is also possible to find such relations for algebraic datatypes. In the following derivations the type declarations (right side of colons) in the type inference rules are structurally the same as the inference rules of propositional logic presented next to them.

Construction of values of sum type (here: two constructors Inl and Inr, each taking an argument of different type) corresponds to introduction of disjunctions (∨I):

Pattern matching on values of sum type corresponds to elimination of disjunctions (∨E):

Construction of values of product type (pairs) corresponds to introduction of conjunctions (∧I):

And finally, decomposition of pairs corresponds to elimination of conjunctions (∧E):

Considering this relation, the type of the data in attribute-value representations would correspond to propositions that are in conjunctive normal form (CNF), i.e. conjunctions of disjunctions, whereas algebraic datatypes relate to arbitrary propositions involving these logical connectives. Any formula in propositional logic can be translated to CNF, but as is well known, this may require exponential space (and hence time) in the worst case²⁵. This, too, shows that our more general representation can yield exponential improvements over attribute-value encodings concerning size of unambiguous representation of structured data and induced models.

The demonstrated correspondence may henceforth be used to convert induced functional programs involving algebraic datatypes to proofs of logical propositions. Since logical propositions are especially relevant for complexity analysis within the PAC-framework of computational learning theory²⁶, this bridge between two fields of research in machine learning may turn out to be very fertilizing.