Read the Stdm User Manual
Contents
1. False gt False False True gt True True False gt True True True gt True Finally the not function performs logical negation not Bool gt Bool not False gt True not True gt False The Stdm file also provides the following operators which look more like the standard mathematical symbols gt lt gt gt N YN gt Bool gt Bool gt Bool The operator is logical and and is exactly equivalent to amp amp The operator is logical or and is exactly equivalent to The gt operator is logical implication and lt gt is logical equivalence For example True lt gt True gt True True lt gt False gt False False gt True gt True True gt False gt False Using the Proof Checker Propositions The basic propositions are logical constants and variables these may be written in any of the following ways e FALSE e true a logical variable A B C Z e a logical variable with any name you like to choose written as Pvar name Notice that the two constants FALSE and true are written differently We ll look into the reason for this in more detail later but for the time being just make sure that you write these two values in the correct way The logical operators are used to construct larger propositions from smaller ones Such propositions can be written in any of the following ways e PAQ writt2. gt True setEq 1 2 3 3 2 1 gt True setEq 1 2 3 3 1 2 gt True If a list used to represent a set contains no duplicate elements then it is said to be in normal form The normalForm function decides whether a set representation is in normal form and the normalizeSet function takes a list and puts it into normal form by removing any duplicate elements The order of elements is immaterial gt normalForm Eq a Show a gt a gt Bool normalForm 1 2 3 gt True normalForm 1 2 3 2 gt False gt normalizeSet Eq a gt a gt Set a normalizeSet 1 2 3 gt 1 2 3 normalizeSet 1 2 3 2 gt 1 3 2 Set union is calculated by the operator thus a Ub would be written in Haskell as a b gt Eq a Show a gt Set a gt Set a gt Set a 1 2 3 2 3 4 gt 1 2 3 4 The operator for set intersection is so a N b is written as a b gt xxx Eq a Show a gt Set a gt Set a gt Set a 1 2 3 2 3 4 gt 2 3 1 2 xxx 3 4 gt The operator denotes set difference thus a b where a and b represent sets is expressed as a b gt 777 Eq a Show a gt Set a gt Set a gt Set a 20 The operator is used to calculate the complement of a set a with respect to a universe u this is expressed as u a and the value is equal to u s If you re doing many calculations with the same universe u
3. n 1 factorial n The first of these examples just uses the first equation factorial 0 1 the others require one or more applications of the second equation In all cases the evaluation stops with the base case the first equation factorial 0 gt 1 factorial 1 gt 1 factorial 5 gt 120 Recursion Over Lists Here is the quicksort algorithm as presented in the book quicksort Ord a gt a gt a quicksort quicksort splitter xs quicksort y y lt xs y lt splitter splitter quicksort y y lt xs y gt splitter VVVVNV NM The following examples test quicksort on several input lists but it is clear that testing can never establish the correctness of the function there are simply too many possible inputs to try them all We would need to prove its correctness mathematically using induction 23 quicksort 3 5 4 gt 3 4 5 quicksort 5 2 9 3 1 6 0 4 8 7 gt 0 1 2 3 4 5 6 7 8 9 quicksort bat ant mouse dog gt ant bat dog mouse Notice that quicksort is not restricted to sorting lists of numbers the last example uses it to sort a list of strings As the type says quicksort can handle lists of any type a as long as a is in the Ord class that is the order operations can be applied to values of type a Compare this with what you have to do in conventional programming languages The book gives firsts as another example of recursion here it
4. s called firsts1 However the recursion pattern of firsts1 is expressed exactly by the map function and it s better programming style to use map directly as in the alternative definition firsts2 gt firstsi firsts2 a b gt al gt firstsi 0 gt firstsi a b ps a firstsi ps gt firsts2 xs map fst xs firstsi cat 4 dog 8 mouse 2 gt cat dog mouse firsts2 cat 4 dog 8 mouse 2 gt cat dog mouse Higher Order Recursive Functions Recursion Over Trees There is really just one sensible way to define lists so Haskell provides lists are a pre defined type with a rich family of functions and operators In contrast there are many ways to define trees and it isn t reasonable to try to include them all in the standard libraries Consequently you need to define your own tree types when programming Here is the version of trees used in the book gt data Tree a gt Tip gt Node a Tree a Tree a gt deriving Show The following definition gives the names t1 and t2 to a couple of specific trees which will be used in several of the following examples Try evaluating t1 and t2 interactively 24 t1 t2 Tree Int t1 Node 6 Tip Tip t2 Node 5 Node 3 Tip Tip Node 8 Node 6 Tip Tip Node 12 Tip Tip VVVV MV This function is a typical recursion over trees it counts the number of Node con structors in a tree Notice that there i
5. AndEL Assume And P Q P gt p4 PIQ amp R PIQ gt AndEL Assume And Or P Q R Or PQ Invalid proofs using And Elimination 1 gt pd p amp q l p gt AndEL Assume Or P Q P gt p6 p amp q l p gt AndEL Assume And P Q Q gt p7 P amp Q R gt AndEL Assume And P Q R Valid proofs with Imp Introduction gt p81 P Q Pag gt AndI Assume P Assume Q gt And P Q 15 VVV VW VVV MV VVV VW v VWVVvVOyvVvVovV VV V VOM VWVVWvVOvVvVvovVV Vo V VOM p82 Q l P gt P amp Q ImpI AndI Assume P Assume Q And P Q Imp P And P Q p83 Q gt P gt P amp Q ImpI ImpI AndI Assume P Assume Q And P Q Imp P And P Q Imp Q Imp P And P Q Valid proofs with Imp Elimination p9 ImpE Assume P Assume Imp P Q Q Here is the theorem and proofs that are used in the book run them like this check_proof example_theorem proof1 should be valid check_proof example_theorem proof2 should give error message example_theorem Theorem example_theorem Theorem Imp Q Imp And P R And R Q proofl Impl ImpI AndI AndER Assume And P R R Assume Q And R Q Imp And P R And R Q Imp Q Imp And P R And R Q The following proof is incorrect proof because Q was inferred where R was needed proof2 Impl ImpI AndI Assume Q AndER Assume And P R R And R Q Imp A
6. Succ Succ Succ Succ Succ Zero And here is subtraction gt sub Peano gt Peano gt Peano gt sub a Zero a gt sub Zero b Zero gt sub Succ a Succ b sub a b sub six four gt Succ Succ Zero sub five one gt Succ Succ Succ Succ Zero Testing for equality is similar Notice that we don t use the built in Haskell operator instead we use recursion gt equals Peano gt Peano gt Bool gt equals Zero Zero True gt equals Zero b False gt equals a Zero False gt equals Succ a Succ b equals a b equals two three gt False equals four four gt True equals add one two sub six three gt True equals sub four two add two three gt False As one last example here is the 1t function which computes the lt relation 21 gt lt Peano gt Peano gt Bool gt lta Zero False gt lt Zero Succ b True gt 1t Succ a Succ b lt ab 1t two three gt True 1t four four gt False 1t add one three sub five four gt False lt add two Zero add three two gt True gt data List a Empty Cons a List a Data Recursion The following function f datarec takes a value and builds a list containing that value repeatedly In the book we simply call this function In most programming languages this function would go into an infinite loop Haskell however uses lazy evaluation which allows s
7. The AFR rule is similiar using instead the AndER constructor Inferences on the Or operator The Or Introduction rule has two forms the left form says that given a you can infer a V b for arbitrary b and the right form says that you if you are given b then you can infer a V b 13 a Re VIR a V b a V b arc bre VE Inferences on Implication ar b gt 21 a b a a b Inferences on Identity and False a tID False CTR a False AA a The Proof Checker uses the following algebraic data type to represent inferences and proofs gt data Proof gt Assume Prop AndI Proof Proof Prop AndEL Proof Prop AndER Proof Prop OrI1 Proof Prop OrI2 Proof Prop OrE Proof Proof Proof Prop NotE Proof Proof Prop ImpI Proof Prop ImpE Proof Proof Prop deriving Eq Show VVVNVV VV Vo VoV 14 Represention of Proofs gt gt gt gt gt AndER gt Assume And P R gt R gt Assume Q gt And R Q gt Imp And P R And R Q gt Imp Q Imp And P R And R Q Valid proofs using And Introduction Theorem 1 q rFqAr proof1 AndI Assume Q Assume R And Q R Invalid proofs using And Introduction gt p2 q r q amp s gt AndI Assume Pvar q Assume Pvar r gt And Pvar q Pvar s Valid proofs using And Elimination 1 gt p3 p amp q l p gt
8. mathematics instructors guide 5 Running Haskell 98 The software tools are written in the standard language Haskell 98 Most of the implementations of Haskell support experimental extensions to the language as well as the standard so it s important to tell the implementation to use Haskell 98 The software uses the literate programming conventions of Haskell This means that every line which begins with the gt character will be compiled but all other lines are comments We recommend that you use the Haskell interpreter Hugs To start Hugs in the Haskell 98 mode start it with the following command hugs 98 Chapter 1 Introduction to Haskell Everything covered in this chapter is a feature of the Haskell 98 language and Stdm doesn t contain any specific definitions relating to the chapter Chapter 2 Propositional Logic Haskell uses the Bool type to represent propositional values There are two constants of type Bool called True and False Be sure to make the first letter upper case Logical Operators Haskell provides several built in logical operators using the Bool type The amp amp operator performs the logical and operation A 887 Bool gt Bool gt Bool False amp amp False gt False False amp amp True gt False True amp amp False gt False True amp amp True gt True The operator performs the logical or operation V Bool gt Bool gt Bool False
9. you can define a specific complement function specialised to that universe as compl u gt Eq a Show a gt Set a gt Set a gt Set a 2 4 1 5 1 5 1141 2 4 gt 1 3 5 The powerset function returns the set of all subsets of its argument If a set contains k elements then its powerset will contain 2 elements gt powerset Eq a Show a gt Set a gt Set Set a powerset Int gt powerset 1 gt 1 powerset 1 2 3 gt 1 2 3 1257 31 1 2 3 2 8750 A minor point in the first example above where we take the powerset of the empty set we declare the type of explicitly This doesn t have anything to do with the mathematics it s just a way of telling the Haskell typechecker what set type we are using The crossproduct function computes the set a x b consisting of the set of all pairs where the first element belongs to a and the second element belongs to b That is axb x y zeaAyEd gt crossproduct gt Eq a Show a Eq b Show b gt gt Set a gt Set b gt Set a b crossproduct 1 2 7 8 9 gt 1 7 1 8 1 9 2 7 2 8 2 9 21 22 Chapter 5 Recursion The factorial function is a typical example of a recursive definition It has two equations one for the base case 0 and one for the recursive case n 1 gt factorial Integer gt Integer gt factorial 0 1 gt factorial n 1
10. Eq a Show a gt Digraph a gt Set a greatestSet Eq a Show a gt Digraph a gt Set a isQuasiOrder Eq a Show a gt Digraph a gt Bool isChain Eq a Show a gt Set a a gt Bool isLinearOrder Eq a Show a gt Digraph a gt Bool removeFromRelation Eq a Show a gt a gt Set a a gt Set a a removeElt Eq a Show a gt a gt Digraph a gt Digraph a topsort Eq a Show a gt Digraph a gt Set a isEquivalenceRelation Eq a Show a gt Digraph a gt Bool 36 Chapter 9 Functions gt isFun Eq a Eq b Show a Show b gt VVVV NM Set a gt Set b gt Set a FunVals b gt Bool data FunVals a Undefined Value a deriving Eq Show isPartialFunction Eq a Eq b Show a Show b gt Set a gt Set b gt Set a FunVals b gt Bool imageValues Eq a Show a gt Set FunVals a gt Set a isSurjective Eq a Eq b Show a Show b gt Set a gt Set b gt Set a FunVals b gt Bool isInjective Eq a Eq b Show a Show b gt Set a gt Set b gt Set a FunVals b gt Bool functionalComposition Eq a Eq b Eq c Show a Show b Show c gt Set a FunVals b gt Set b FunVals c gt Set a FunVals c gt isBijective Eq a Eq b Show a Show b gt Set a gt Set b gt Set a FunVals b gt Bool isPermutation Eq a Show a gt Set a gt Set a gt Set a FunVals a g
11. Software Tools for Discrete Mathematics User Manual Cordelia Hall and John O Donnell Last modified April 11 2000 The Home Page for the book from which you can obtain this document as well as the software Stfm 1hs is available on the Web at www dcs gla ac uk jtod discrete mathematics Copyright 2000 by Cordelia Hall and John O Donnell Contents O Getting Started 5 Web Addresses o c 2 osu a te a ca RR Rw 5 Instructors Ge 5 esar as den me we a ae 5 Kinos Haskel O8 Sis ios HE an EE SER Ts EERE 6 1 Introduction to Haskell 7 2 Propositional Logic 9 Logical Operators 22 54 22 u au an OEE ES EERE ESE 9 Using the Proof Checker o o aoc ba ee bu ee A 10 Pree es e cara Sas as E 10 Theorems A 11 o AI 12 o SR 12 Inferences on the And operator 4 4 aa ias 12 Inferences on the Or operator su a u ede eee tee we deen 13 Inferences on Implication 2 0 4 4 2654465 fe eee eee ee ees 14 Inferences on Identity and False 14 Represention of Proofs oc cc cesca tat ru bbw ra med 15 3 Predicate Logic 17 4 Set Theory 19 5 Recursion 23 Recursion yer ee ee Ye ee eh ee RES Oe EES Ow ERE HS 23 Higher Order Recursive Functions o 4 au ec oo 2224944848545 due 24 Recursion yer Trees a cca du cte an a de EERE RSR mE EHS 24 Penne Afithmetie sa o es aa be a amp DRE Set Reo A 26 Data Recursion e sos eat BASRA re Bar Brei 28 6 Inductively Defined Set
12. d function looks up a number in the database if that number is found in the first element of a pair then the second element is returned gt find Int gt Tree Int a gt Maybe a gt find n Tip Nothing gt find n Node m d t1 t2 gt if n m then Just d gt else if n lt m then find n tl gt else find n t2 find 6 tree gt Just 12 find 7 tree gt Just 14 find 20 tree gt Nothing Peano Arithmetic Peano represents natural numbers that is the non negative integers gt data Peano Zero Succ Peano deriving Show The following definitions will be used soon in several examples Try evaluating them interactively Notice that that the Peano representation of k always contains exactly k occurrences of Succ gt one Succ Zero gt two Succ one gt three Succ two gt four Succ three gt five Succ four gt six Succ five The decrement function can be defined simply by pattern matching 26 gt decrement Peano gt Peano gt decrement Zero Zero gt decrement Succ a a As an example notice that decrement six produces the represenation of five five gt Succ Succ Succ Succ Succ Zero decrement six gt Succ Succ Succ Succ Succ Zero Most operations in Peano arithmetic must be defined using recursion addition is a typical example gt add Peano gt Peano gt Peano gt add Zero b b gt add Succ a b Succ add a b add two three gt
13. e suppose we are working on the theorem P Q F PAQ As we ll see shortly the key step will be an inference using the AT rule but that inference will require us to have established the propositions P and Q The statement that P has been established by assuming it is written Assume P If this statement is used in the proof of a theorem then P must appear in the list of assumptions unless the assumption has been discharged Inferences on the And operator 12 a b a Ab a Ab AI AEr NER a a avb arc bre vIr VIR VE avb a V b c aF b a a b I gt E a b b a False a False ID CTR RAA a a a Figure 2 1 Inference Rules of Propositional Logic The And Introduction rule AJ says that if two propositions a and b have been established then their conjunction a Ab can be inferred a M AT a Ab This inference is written in the form AndI Proof Proof Prop There are two And Elimination rules the left and right versions In both cases the rule s assumption is that a conjunction of the form a Ab has been established The left rule AE says that the leftmost part of the conjunction a can be inferred while the right rule A ER says that b may be inferred a b a b NEL AER a An inference using the AE rule is written as AndEL followed by a proof of the con junction a A b followed by the proposition a
14. en as either And P QorasP And Q e PV Q written as either Or P QorasP Or Q 10 Table 2 1 Examples of Proposition Representation P P PVQ Or PQ P Or Q PAQ And P Q P And Q PAQ V RAS Or And P Q And R S P And Q Or R And 8 e P Q written as either Imp P QorasP Imp Q e P written as Not P Parentheses are needed when the areguments to a logical operator are themselves expressions For example we can write PAQ as And P Q without parentheses but the expression P Q V R would be written as Or And P Q R where the parentheses are essential An alternative way to write this is P And Q Or R but here again the parentheses are required to indicate the structure of the expression Theorems A theorem in propositional logic always has a standard form it says that a proposition p can be inferred from a set of assumptions ag 1 ax_1 The mathematical notation for this is Q0 41 Ak 1 D For example the theorem P QEPAQ has two assumptions P and Q and the conclusion is PAQ This statement means given the assumptions P and Q it is possible to infer the conclusion P AQ The number k of assumptions may be 0 thus the theorem HP P says that P P can be proved without making any assumptions at all To represent a theorem in Haskell write Theorem followed by a list of assumptions followed by the proposition which the
15. nd P R And R Q Imp Q Imp And PR And R Q 16 Chapter 3 Predicate Logic Soon there will be more about this gt forall Int gt Int gt Bool gt Bool gt exists Int gt Int gt Bool gt Bool 17 18 Chapter 4 Set Theory A set will be represented as a list gt type Set a a The subset function takes two sets as arguments and returns True if the first is a subset of the second Note the function does not reject non sets gt subset Eq a Show a gt Set a gt Set a gt Bool subset 4 3 1 2 3 4 5 gt True subset 9 3 1 2 3 4 5 gt False subset 1 2 3 4 5 1 2 3 4 5 gt True subset gt True The properSubset function implements C it is just like subset except that it returns False if the first argument is equal to the second Note that properSubset does not reject non sets gt properSubset Eq a Show a gt Set a gt Set a gt Bool properSubset 4 3 1 2 3 4 5 gt True properSubset 9 3 1 2 3 4 5 gt False properSubset 1 2 3 4 5 1 2 3 4 5 gt False x DIFFERENT FROM subset properSubset gt True The setEq function determines whether the two arguments represent the same set They are equal if they contain the same elements regardless of the order 19 gt setEq Eq a Show a gt Set a gt Set a gt Bool setEq 1 2 3 2 3 4 gt False setEq 1 2 3 1 2 3
16. s 31 7 Induction 33 8 Relations 35 9 Functions 37 10 Digital Circuit Design 39 Chapter 0 Getting Started Welcome to the User s Manual for the Software Tools for Discrete Mathematics To use this software you should obtain e The book Discrete Mathematics Using a Computer by Cordelia Hall and John O Donnell Published by Springer in January 2000 16 95 Softcover 360 pages ISBN 1 85233 089 9 e The DMC Home Page on the Web which contains general information as well as direct links to the following items e The software Stdm 1hs a source file in the Haskell 98 programming language e This manual which is available on the web in pdf format The software this manual and the web resources are intended to be used along with the book This isn t a self contained standalone document Web Addresses If you re reading this document online you can find everything you need by following the hyperlinks above If you re reading this on paper however you may need the Web URL addresses for 1 the DMC Home Page 2 the software file Stfm 1hs and 3 this manual pdf format www dcs gla ac uk jtod discrete mathematics www dcs gla ac uk jtod discrete mathematics Stdm lhs www dcs gla ac uk jtod discrete mathematics StdmMan pdf Instructor s Guide If you are teaching a course using these materials you should also obtain access to the Instructor s Guide whose URL is www dcs gla ac uk jtod discrete
17. s a base case and a recursion case just as for list functions but here the recursion case must call nodeCount twice since there are two subtrees under a Node gt nodeCount Tree a gt Int gt nodeCount Tip 0 gt nodeCount Node x ti t2 1 nodeCount t1 nodeCount t2 nodeCount ti The reflect function is a particularly elegant example of recursion gt reflect Tree a gt Tree a gt reflect Tip Tip gt reflect Node a t1 t2 Node a reflect t2 reflect t1 reflect t1 gt Node 6 Tip Tip reflect t2 gt Node 5 Node 8 Node 12 Tip Tip Node 6 Tip Tip Node 3 Tip Tip For any data structure we can define a map operation that applies some function f to every element of the structure Here is the mapTree function which applies f a gt b to every element in a Tree gt mapTree a gt b gt Tree a gt Tree b gt mapTree f Tip Tip gt mapTree f Node a t1 t2 gt Node f a mapTree f t1 mapTree f t2 mapTree 10 t1 gt Node 60 Tip Tip mapTree 10 t2 gt Node 50 Node 30 Tip Tip Node 80 Node 60 Tip Tip Node 120 Tip Tip 25 This tree stores a pair of type Int Int in every Node rather than just a singleton value This gives us a little database gt tree Tree Int Int gt tree gt Node 5 10 gt Node 3 6 Node 1 1 Tip Tip gt Node 4 8 Tip Tip gt Node 7 14 Node 6 12 Tip Tip gt Node 8 16 Tip Tip The fin
18. t Bool diagonal Int gt Int Int gt Int Int rationals Int Int 37 38 Chapter 10 Digital Circuit Design gt class Signal a where gt inv a gt a gt and2 or2 xor a gt a gt a gt instance Signal Bool where gt inv False True gt inv True False gt and2 amp amp gt or2 I gt xor False False False gt xor False True True gt xor True False True gt xor True True False V halfAdd Signal a gt a gt a gt a a halfAdd a b and2 a b xor a b V fullAdd Signal a gt a a gt a gt a a fullAdd a b c or2 w y z where w x halfAdd a b y z halfAdd x c VVV NM halfAdd False False halfAdd False True halfAdd True False halfAdd True True fullAdd False False False fullAdd False False True fullAdd False True False fullAdd False True True fullAdd True False False 39 fullAdd True False True fullAdd True True False fullAdd True True True Vv VV VNVNV NM VVVNV VM add4 Signal a gt a gt a a gt a a add4 c x0 y0 x1 y1 x2 y2 x3 y3 c0 s0 s1 s2 s3 where c0 s0 fullAdd x0 y0 cl c1 s1 fullAdd x1 y1 c2 c2 s2 fullAdd x2 y2 c3 c3 s3 fullAdd x3 y3 c Example addition of 3 8 3 8 0011 2 1 3 1000 8 8 1011 8 2 1 11 Calculate this by evaluating add4 False False True False False True False Tr
19. t isDigraph Eq a Show a gt Digraph a gt Bool gt digraphEq Eq a Show a gt Digraph a gt Digraph a gt Bool gt isReflexive Eq a Show a gt Digraph a gt Bool gt isIrreflexive Eq a Show a gt Digraph a gt Bool gt lessThan_N100 Digraph Int gt equals_N100 Digraph Int gt greaterThan_N100 Digraph Int gt lessThan0rEq_N100 Digraph Int gt greaterThanOrEq_N100 Digraph Int gt notEg_N100 Digraph Int gt isSymmetric Eq a Show a gt Digraph a gt Bool gt isAntisymmetric Eq a Show a gt Digraph a gt Bool gt isTransitive Eq a Show a gt Digraph a gt Bool gt relationalComposition Show a Eq b Show c Show b Eq c Eq a gt gt Set a b gt Set b c gt Set a c 35 Vv equalityRelation Eq a Show a gt Set a gt Relation a relationalPower Eq a Show a gt Digraph a gt Int gt Relation a reflexiveClosure Eq a Show a gt Digraph a gt Digraph a inverse Set a b gt Set b a symmetricClosure Eq a Show a gt Digraph a gt Digraph a transitiveClosure Eq a Show a gt Digraph a gt Digraph a isPartialOrder Eq a Show a gt Digraph a gt Bool remTransArcs Eq a Show a gt Relation a gt Relation a isWeakest Eq a Show a gt Relation a gt a gt Bool isGreatest Eq a Show a gt Relation a gt a gt Bool weakestSet
20. theorem claims to hold Thus the theorem P QFPAQ would be represented as Theorem P Q P And Q 11 Notice that the two assumptions P and Q are written in a list surrounded by square brackets and separated by commas The order of assumptions in the list doesn t matter The conclusion of the theorem is P And Q but this must be surronded by parentheses because it contains several symbols If a theorem has no assumptions then an empty list of assumptions is specified Thus the theorem PP is written as Theorem P Imp P Usually it is convenient to use an equation to give a name to a theorem put the equation in a file and you can then alternately edit the file and reload it in Hugs as you work with the theorem interactively The book defines example_theorem to be the name of the theorem HFQ PAR RAQ using the following equation which appears in the Stdm 1hs file gt example_theorem Theorem gt example_theorem gt Theorem gt gt Imp Q Imp And P R And R Q The proof checker defines the representation of theorems with the following algebraic data type gt data Theorem gt Theorem Prop Prop gt deriving Eq Show Inferences Assumptions There are two ways to establish a proposition it can be assumed or inferred To express the fact that a proposition p has been established by assuming it we write Assume followed by the Haskell representation of p For exampl
21. uch infinite data structures to be defined usefully The idea is that the Haskell implementation evaluates only the parts of the data structure that are actually required gt f_datarec a gt a gt f_datarec x x f_datarec x The list ones Int is an infinte list of ones gt ones f_datarec 1 Now we try evaluating ones Try it When you get bored with the output you can interrupt the computation and get another interactive prompt from the Haskell inter preter To interrupt the computation on Windows click Stop to interrupt in on Unix type control C ones gt 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 Here is another definition which is essentially the same except that it doen t use a helper function the data structure is defined using data recursion instead of the more ordinary function recursion gt twos 2 twos twos gt 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 28 Any kind of circular data structure can be defined in a similar way gt object let a 1 b gt b 2 c gt c 3 a gt in a object gt 1 2 3 1 2 3 1 2 3 1 2 3 1 2 3 1 2 3 29 30 Chapter 6 Inductively Defined Sets 32 Chapter 7 Induction 34 Chapter 8 Relations gt type Relation a Set a a gt type Digraph a Set a Relation a gt domain Eq a Show a Eq b Show b gt Set a b gt Set a gt codomain Eq a Show a Eq b Show b gt Set a b gt Set b g
22. ue False The expected result is False True False True True mscanr b gt a gt a c gt a gt b gt a c mscanr f a a mscanr f a x xs let a ys mscanr f a xs a y f x a in ka y ys gt rippleAdd Signal a gt a gt a a gt a a rippleAdd c zs mscanr fullAdd c zs Example addition of 23 11 23 11 010111 16 4 2 1 001011 8 2 1 11 with carry input 0 100010 32 2 34 with carry output 0 Calculate with the circuit by evaluating rippleAdd False False False True False False True True False True True True True The expected result is False True False False False True False 23 40
Download Pdf Manuals
Related Search