Maths - Boolean Types

 

We can use sum to get boolean from two units (1+1=2)

Notation

 

Rules

Types are defined by their formation, term introduction, term eliminator and computation rules:

 

Boolean Type

formation rule

dont really need to have two copies of Unit, just making the point this is a sum.

right adjointUnit:Type   right adjointUnit:Type
right adjointBoolean : Type
term introduction rule
Γright adjointa:Unit   Γright adjointb:Unit
Γright adjointinl(a): Boolean   Γright adjointinr(b): Boolean

term eliminator

assume: a implies c
and b implies c

Γright adjointp:Boolean   Γ a:Unitright adjointcA :C   Γ b:Unitright adjointcB :C
Γright adjointmatch(p, a.cA b.cB):C
computation rule

beta reduction

match(inl(a), x.cA y.cB) ->β cA[a/x]

match(inr(b), x.cA y.cB) ->β cB[b/x]

Local completeness rule

 

Idris Code

Idris Code for Boolean is here.

The formation and term introduction rules can be represented simply in Idris like this:

||| Boolean Data Type
data Bool = False | True
The term eliminator can be implemented by the if-then-else construct or perhaps, a bit more generally the 'case' construct.
||| The underlying implementation of the if ... then ... else ... syntax
||| @ b the condition on the if
||| @ t the value if b is true
||| @ e the value if b is false
ifThenElse : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
ifThenElse True  t e = t
ifThenElse False t e = e
computation and local completeness rules
if True then True else False
if False then False else True 

Negation

We can then add negation

formation rule

 

term introduction rule

Pright adjoint_|_
right adjoint¬P
term eliminator  
computation rule  

Local completeness rule

 

Bottom Rule

formation rule

 

term introduction rule

right adjointP ¬P
right adjoint_|_
term eliminator  
computation rule  

Local completeness rule

 

    The formation rule (e.g. Bool : Set)

    The introduction rules (e.g. true : Bool and false : Bool)

    The elimination rules (e.g. if P : Bool -> Set, b : Bool, pt : P true, and pf : P false, then if b then pt else pf : P b)

    The computation rules (e.g. if true then pt else pf = pt and if false then pt else pf = pf)

We can use sum to get boolean from two units (1+1=2)

 

Boolean Type

formation rule

dont really need to have two copies of Unit, just making the point this is a sum.

right adjointUnit:Type   right adjointUnit:Type
right adjointBoolean : Type
term introduction rule
Γright adjointa:Unit   Γright adjointb:Unit
Γright adjointinl(a): Boolean   Γright adjointinr(b): Boolean

term eliminator

assume: a implies c
and b implies c

Γright adjointp:Boolean   Γ a:Unitright adjointright adjointcA :C   Γ b:Unitright adjointright adjointcB :C
Γright adjointmatch(p, a.cA b.cB):C
computation rule

beta reduction

match(inl(a), x.cA y.cB) ->β cA[a/x]

match(inr(b), x.cA y.cB) ->β cB[b/x]

Local completeness rule

 

We can then add negation

Negation Rule

formation rule

 

term introduction rule

Pright adjoint_|_
right adjoint¬P
term eliminator  
computation rule  

Local completeness rule

 

Bottom Rule

formation rule

 

term introduction rule

right adjointP ¬P
right adjoint_|_
term eliminator  
computation rule  

Local completeness rule

 

 

Next Steps

Other types are discussed on the following pages:


metadata block
see also:

http://www.mathreference.com/

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.