Gilles Nies: Bachelor Thesis

Representations of Boolean functions in Constructive Type Theory

Author: Gilles Nies
Advisor: Chad E. Brown
Supervisor: Gert Smolka

Abstract

Boolean functions are an abstraction of one of the most important computer hardware topics: circuits. They can be represented in many different ways like truth tables or logical expressions. While truth tables are often rejected because of their expensiveness in space, logical expressions come with an infinite number of representations for the same Boolean function. We give several definitions of Boolean functions, Decision Trees and Prime Trees in Coq and prove that Prime Trees give a canonical representation of Boolean functions. Sometimes this requires the assumption of consistent, yet unprovable propositions to circumvent some well-known problems in Coq.

Talks

27.09.2011, 15:15: First talk (Building E1 3, Room 528)
04.11.2011, 14:15: Proposal talk (Building E1 3, Room 528)
20.04.2012, 14:15: Final talk (Building E1 3, Room 528) slides

Downloads

Thesis

The finished thesis can be downloaded here.

Coq developments

General results - Some general results.
Isomorphism - This contains all the different ways of definining an isomorphism we thought of.
Version 1: We use cascaded boolean functions and define decision trees as a dependent inductive type and show that the resulting prime trees are isomorphic to cascaded boolean functions.
Version 2: Dependent types are not easy to use. We therefore came up with a recursive definition of decision trees and show that this definition is isomorphic to the above one and provide the whole development using this alternative definition.
Version 3: We fix decision trees as a simple inductive type and use a more classical definition of boolean functions. To show that boolean functions and prime trees are isomorphic we assume the axiom of continuity. We were able to show that this axiom is inconsistent with strong classical logic.
Version 4: Instead of assuming the controversial axiom of continuity we instead assume the axiom of description, an assumption consistent with classical logic. The resulting development can be found here.
Version 5: In this last version we finally provide a development that does not rely on the assumption of axioms.
Instead of using the definitions of boolean functions of versions 3-5, one can also use an isomorphic representation of boolean functions involving streams.

Legal notice, Privacy policy