It's easy as p1, p2, p3, ...

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.

 --}