**Paste:**#108099**Author(s):**1HaskellADay**Language:**Haskell**Channel:**-**Created:**2014-07-25 09:47:20 UTC**Revisions:**- 2014-07-25 09:56:51 UTC #108101 (diff): No title (1HaskellADay)
- 2014-07-25 09:48:58 UTC #108100 (diff): No title (1HaskellADay)
- 2014-07-25 09:47:20 UTC #108099: It's easy as p1, p2, p3, ... (1HaskellADay)

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 | import Prelude hiding (max, min, subtract) {-- Logic. Okay, folks, we're imbarking on Logic in Haskell. Dah-dun-DAAAAAH! So, the next set of problems of the P-99 Prolog problems, that is, P46-P48 get into the syntax and semantics of Boolean logic and its expression, and I'm sure that's utterly fascinating, if I were into now, particularly as I love formulating DSLs ('domain-specific languages') to address particular problem domains naturally, but for now I'm like ... 'eh!' Yeah, I'm feeling the 'eh' for boolean logic right now. I mean, sure, an' b'gorra, you can use boolean logics for interesting things, like CPS (constraint problem solving) or CPS (continuation-passing style ... for boolean logics) or binary ... whatever. But I'm like ... 'eh!' For now, anyway. Maybe (boolean functor, there) next week I'll 'un-eh' myself. Besides, I'm also not feeling the 'build a scanner/parser that ...' I'd rather work IN the language WITH the language to BUILD the language I need to use. After all, that's why they call this language ML ('meta-language'), right? Oops. Wrong language. Did I say 'ML'? I MEANT to say Haskell, 'cause, leik ... Yeah. SO! We're going so the logic here in these next few sets of exercises, but not (just) Boole(an) logic (Hi, George!). No, I'm thinking another 'G'-logic: Gödel. Oh, yeah. We just went there. Fasten your seatbelts, passengers, we're in for some turbulence ahead. So, our Mr. G-man G was able to reduce expressibility of logic down to a few symbols, and then encode those symbols into numbers and then prove that lattes at Starbucks would now cost MORE THAN FIVE DOLLARS FOR A CUP OF COFFEE, AND WHY IS THAT SANE IN ANYONE'S BOOK? LIKE: EVER? Um, no. Actually, he didn't prove that. He proved something else, but I think his theorem was incomplete, so I'll wait for him to finish it before we cover it here. Heh. ANYWAY! So, we can go all Gödel-numbering, right here, right now, but we won't. INSTEAD, what we'll do here is a bit of exploration of logic (but FUN-logic!) with a minimal subset of the language of Haskell, we'll call it "H'" perhaps? or "HA!"? I'm kinda liking the 'HA!' language-name... And the reason we'll do that is because of natural curiosity and inquisitive nature (natural-nature) has lead me to wonder some things around beauty, simplicity, austerity, and rigor (or 'rigour,' if you prefer). And you get to ... do this. Isn't that JUST PEACHY? You're welcome. SO! Gödel had a minimal set of symbols on his language, P, and with those symbols he could write any computable function, or, put another way, any provable ('inhabitable') sentence in his logical universe, P. P is for 'Peano Arithmetic.' Note that I said 'inhabitable,' as this is the crux of his logic, and the logic he used was intuitionistic logic, where there's no concept of 'true' or 'false' but only inhabitability. A sentence is proved if it's inhabited and it's not provable if there are no inhabitants to be found. The neat thing about intuitionistic logic (that doesn't have 'none' or 'false' or 'bottom'), as opposed to classical logic, is that there's a one-to-one correspondence between intuitionistic logic and ... well, computer programs. A proof in intuitionistic logic can be represented by a transliterated program in ... um ... intuitionistic logic? ... which is nice, since some programming languages use intuitionistic type theory as a basis for their type systems. Groovitude! 'Eh,' you say, 'so what?' Well, the neat thing for me is this: if you have an inhabited statement or set of statements expressed in intuitionistic logic, then the transliteration, if it's faithful, is PROVED correct in the corresponding programming language. And that's a pretty sweet place to start from, where your program is proved correct. But what can you do with it? Well, if you have that and five USD, you can buy a cup of coffee at Starbucks, right? Sweet! *AHEM* Moving on. Gödel's minimal set of symbols were: "Formalization of Gödel numbering, the symbols: 0, 1, +, x, =, (, ), ^ (and), ¬, ∀, and var(x) [for x = 0, 1, 2, ...]. All logic can be expressed with those symbols" (that's from a tweet from somebody I know ... intimately) But that's not even the MINIMAL-minimal, as we have from Combinator logic: "In combinator logic, the two symbols: Sabc = ab(ac), Kab = a are sufficient to express any proposition in logic." And in Haskell, those two symbols are 'easy' to represent, as K is const and S is ... well, something else. But the MINIMAL-minimal isn't even the MINIMAL-MINIMAL-MINIMAL, as there is the nand-logic that has just one symbol (NAND), or you could go with the NOR-logic, if you prefer that one, instead, so there are 1-symbol logics (and even combinator logic has an universal N-logic (the 'Nightingale'-combinator that Smullyan discusses in his To Mock a Mockingbird meditation). And, to go one further, there are the OISC and NoISC instruction sets (OISC: one-instruction, DJNZ -- 'decrement-jump- not-zero' and NoISC: no-instruction set). But we're not going there (now), as sentences in SK-logic are rather lengthy and rather more of a challenging puzzle to discern, just by looking at them. Instead we're going here, because, logically, here we are. The HA!-instruction set. Given the symbols: S Z ( ) = :: -> fx nx (for x = 0, 1, 2 ...) BUT NOT! undefined, as I'm the language-creator, and _I_ can use 'undefined,' but you can't, because I deem it a too-powerful construct for you to use safely or reasonably. But I can use it. But you can't. Does that sound ... familiar, at all, to anyone? where the semantics of fx is a function name and nx is a variable name, the semantics (the type) of S Z are Peano and ( ) = are as in Haskell. And we have, so far, the type system inhabited by the type-assignment ::, and the types Peano, Peano -> Peano, Peano -> Peano -> Peano, ... and, optionally, the function-types (Peano -> Peano), (Peano -> Peano) -> Peano, and variations of those. But we don't have to concern ourselves with function-types here in this non-bonus-like exercise set. We're good. Besides. Pfft! Who needs function-types, anyway? Yeah. *AHEM* I'll also throw in pattern matching and application-as-juxtaposition for free for ya, 'cause I'm that nice. You're welcome. Remember no 'where' is to show nowhere in the code. Geddit? 'no-where' 'nowhere'? GEDDIT? So, given the above, and given the following predefined type (in this magical- metalanguage of HA! called ... 'Haskell,' so don't get any ideas about user- defined types, because ... why would users want to defined their own types when addition on the Peano-numbers is Turing-complete, huh?): --} data Peano = Z | S Peano -- So, yeah, given the above, write the following functions: max :: Peano -> Peano -> Peano max n1 n2 = undefined min :: Peano -> Peano -> Peano min n1 n2 = undefined add :: Peano -> Peano -> Peano add n1 n2 = undefined subtract :: Peano -> Peano -> Peano subtract n1 n2 = undefined -- ... for subtract, please note the Peano-semantics of the lower-bound -- of the series: pred Z = Z also please note that 'pred' is not a predefined -- function in HA!) -- ... Now for mult and pow there are more direct ways to do these, but -- that involves Church-numerals, and we would never do that to you. Oh, no! -- ... Yeah, just the Peano-representation. Here. -- (heheheh) mult :: Peano -> Peano -> Peano mult n1 n2 = undefined pow :: Peano -> Peano -> Peano pow n1 n2 = undefined fact :: Peano -> Peano fact n0 = undefined {-- Please note some things. There's no 'if,' nor 'then,' nor 'else,' in HA! There's no '+' nor '*' nor even '**' in HA! There's no 'where' in HA! I have loosened the restrictive function naming of f0, f1, f2 to be ... well, the qualified-naming convention for Haskell names. You're welcome. Also, for the a show-representation of Peano you may use an alternative representation, like, for example: S (S (S Z)) could have a representation of "P3" if you wish. Exercise. Do that. But in the 'meta-language' of HA! called ... 'Haskell,' oddly enough. --} {-- geophf walks away. --} {-- geophf walks back. Oh, and to be complete about this (although with addition and destructuring I suppose one could argue we are complete, already...), define the following isomorphic and comparative operators: No. Wait. For equality and other truth-operators, we need some agreement on 'what is truth.' "What is truth?" Pontius Pilate asked. There are some who say that he didn't like the non-answer he got. --} data Boolean {- as in George -} = Sure | Whatevs -- 'Whatevs' always means 'No' deriving (Eq, Show, Read) -- have you noticed that? -- a passive-aggressive 'No' eq :: Peano -> Peano -> Boolean eq n1 n2 = undefined lt :: Peano -> Peano -> Boolean lt n1 n2 = undefined {-- Now, with eq and lt defined, and the Boolean type in place, you can define the other truth operators on Peano numbers in relation to them, right? Do that. Define the other Peano comparator-operators in relation to only lt and eq ... and possibly some other Boolean-function you, the intrepid logician, declare yourself. --} le :: Peano -> Peano -> Boolean le n1 n2 = undefined gt :: Peano -> Peano -> Boolean gt n1 n2 = undefined ge :: Peano -> Peano -> Boolean ge n1 n2 = undefined {-- Please note, that it is convenient, but not strictly necessary, to have a Boolean-type distinct from the Peano numbers as it is possible that Boolean can be represented (and dispatched against) as a choice of Peano numbers. And when I say 'convenient,' I mean 'really convenient from a (type-) declaration perspective convenient.' For, after all: eq :: Peano -> Peano -> Peano doesn't tell us much, declaratively, as eq :: Peano -> Peano -> Boolean amirite? But there are some who claim that typing things makes programming harder. Uh, huh. I agree: writing things correctly is harder than ... not. Just my opinion. --} |