Andrew Cooke | Contents | Latest | RSS | Previous | Next

C[omp]ute

Welcome to my blog, which was once a mailing list of the same name and is still generated by mail. Please reply via the "comment" links.

Always interested in offers/projects/new ideas. Eclectic experience in fields like: numerical computing; Python web; Java enterprise; functional languages; GPGPU; SQL databases; etc. Based in Santiago, Chile; telecommute worldwide. CV; email.

Personal Projects

Choochoo Training Diary

Last 100 entries

Surprise Paradox; [Books] Good Author List; [Computing] Efficient queries with grouping in Postgres; [Computing] Automatic Wake (Linux); [Computing] AWS CDK Aspects in Go; [Bike] Adidas Gravel Shoes; [Computing, Horror] Biological Chips; [Books] Weird Lit Recs; [Covid] Extended SIR Models; [Art] York-based Printmaker; [Physics] Quantum Transitions are not Instantaneous; [Computing] AI and Drum Machines; [Computing] Probabilities, Stopping Times, Martingales; bpftrace Intro Article; [Computing] Starlab Systems - Linux Laptops; [Computing] Extended Berkeley Packet Filter; [Green] Mainspring Linear Generator; Better Approach; Rummikub Solver; Chilean Poetry; Felicitations - Empowerment Grant; [Bike] Fixing Spyre Brakes (That Need Constant Adjustment); [Computing, Music] Raspberry Pi Media (Audio) Streamer; [Computing] Amazing Hack To Embed DSL In Python; [Bike] Ruta Del Condor (El Alfalfal); [Bike] Estimating Power On Climbs; [Computing] Applying Azure B2C Authentication To Function Apps; [Bike] Gearing On The Back Of An Envelope; [Computing] Okular and Postscript in OpenSuse; There's a fix!; [Computing] Fail2Ban on OpenSuse Leap 15.3 (NFTables); [Cycling, Computing] Power Calculation and Brakes; [Hardware, Computing] Amazing Pockit Computer; Bullying; How I Am - 3 Years Post Accident, 8+ Years With MS; [USA Politics] In America's Uncivil War Republicans Are The Aggressors; [Programming] Selenium and Python; Better Walking Data; [Bike] How Fast Before Walking More Efficient Than Cycling?; [COVID] Coronavirus And Cycling; [Programming] Docker on OpenSuse; Cadence v Speed; [Bike] Gearing For Real Cyclists; [Programming] React plotting - visx; [Programming] React Leaflet; AliExpress Independent Sellers; Applebaum - Twilight of Democracy; [Politics] Back + US Elections; [Programming,Exercise] Simple Timer Script; [News] 2019: The year revolt went global; [Politics] The world's most-surveilled cities; [Bike] Hope Freehub; [Restaurant] Mama Chau's (Chinese, Providencia); [Politics] Brexit Podcast; [Diary] Pneumonia; [Politics] Britain's Reichstag Fire moment; install cairo; [Programming] GCC Sanitizer Flags; [GPU, Programming] Per-Thread Program Counters; My Bike Accident - Looking Back One Year; [Python] Geographic heights are incredibly easy!; [Cooking] Cookie Recipe; Efficient, Simple, Directed Maximisation of Noisy Function; And for argparse; Bash Completion in Python; [Computing] Configuring Github Jekyll Locally; [Maths, Link] The Napkin Project; You can Masquerade in Firewalld; [Bike] Servicing Budget (Spring) Forks; [Crypto] CIA Internet Comms Failure; [Python] Cute Rate Limiting API; [Causality] Judea Pearl Lecture; [Security, Computing] Chinese Hardware Hack Of Supermicro Boards; SQLAlchemy Joined Table Inheritance and Delete Cascade; [Translation] The Club; [Computing] Super Potato Bruh; [Computing] Extending Jupyter; Further HRM Details; [Computing, Bike] Activities in ch2; [Books, Link] Modern Japanese Lit; What ended up there; [Link, Book] Logic Book; Update - Garmin Express / Connect; Garmin Forerunner 35 v 230; [Link, Politics, Internet] Government Trolls; [Link, Politics] Why identity politics benefits the right more than the left; SSH Forwarding; A Specification For Repeating Events; A Fight for the Soul of Science; [Science, Book, Link] Lost In Math; OpenSuse Leap 15 Network Fixes; Update; [Book] Galileo's Middle Finger; [Bike] Chinese Carbon Rims; [Bike] Servicing Shimano XT Front Hub HB-M8010; [Bike] Aliexpress Cycling Tops; [Computing] Change to ssh handling of multiple identities?; [Bike] Endura Hummvee Lite II; [Computing] Marble Based Logic; [Link, Politics] Sanity Check For Nuclear Launch; [Link, Science] Entropy and Life

© 2006-2017 Andrew Cooke (site) / post authors (content).

TTFP Exercises

From: "andrew cooke" <andrew@...>

Date: Mon, 23 Jan 2006 00:27:16 -0300 (CLST)

ere's my initial attempt at the first few exercises in TTFP (Type Theory
and Functional Programming; see posts at
http://www.acooke.org/cute/MoreConstr0.html).  Hopefully I'll keep
updating this thread as I get further through the book.

Notation:
- for negation
! for bottom (the uspide down T)
So -X is equivalent to X => !

1.1 Prove transivity of implication

[A]1  A => B
------------ (=> E)
     B                B => C
---------------------------- (=> E)
             C
          ------ (=> I1)
          A => C

((A => B) => (B => C)) => (A => C)

Note that it's OK to introduce extra propositions (like A above) at the
start, as long as you eliminate them later (this is what "elimination"
means)


1.2 Prove ((A u B) => C) => ((A => C) n (B => C))

                         (A u B) => C
             ---------------------------------------------- (n I)
             (A u B) => C        n             (A u B) => C
[A]1            .                . [B]2            .
----- (u I)     .                . ----- (u I)     .
A u B           .                . A u B           .
------------------------- (=> E) . ------------------------- (=> E)
          C                      .           C
       ------ (=> I1)            .        ------ (=> I2)
       A => C                             B => C

So ((A u B) => C) => ((A => C) n (B => C))


1.3 Prove (A => (B => C)) => ((A n B) => C)

[A n B]1
-------- (n E x 2)
 B   A
 .   .
 .   .  (A => (B => C))
 .   ------------------ (=> E)
 .           B => C
 ------------------ (=> E)
          C
    ------------ (=> I)
    (A n B) => C


1.4 Joke question?
[later] - book author (Simon Thompson) replied saying it was a mistake!


1.5 Prove (B u C) => -(-A n -B)

This looks so much like De Morgan's law I'm going to assume it's a typo
and instead prove (A u B) => -(-A n -B)

However, I can't find a solution (looks like it needs the excldued middle?)


1.6 (a) Prove ((A => B) n (A => -B)) => -A

 [A]1  A => B         [A]1  A => (B => !)
 ------------ (=> E)  ------------------- (=> E)
      B                      (B => !)
      ------------------------------- (=> E)
                    !
                  ------ (=> I1)
                  A => !

I'm not that sure about this because it might contradict (! E):
  !
 ---
  X
I think it doesn't because there's "more above" than just !.

Also, there are assumptions about how the "deduction process" corresponds
to a formula:
 - n being implicit between different "tracks" in the argument (OK, I
   think, since n appears to be associative and commutative).
 - vertical steps being equivalent to =>

(b) Prove (A n -A) => B

A  (A => !)
----------- (=> E)
     !
    --- (! E)
     B

Question 1.7

From: "andrew cooke" <andrew@...>

Date: Tue, 24 Jan 2006 11:36:44 -0300 (CLST)

1.7 Show the equivalence of EM/DN/CC

I can't find a way to do this starting with the EM formula given and
generating the other expressions.  And I think I can explain why (see Note
at foot of this for a resolution of this problem):

The law of the excluded middle (Boolean logic; I'm not sure what the
difference is) asserts *two* things about the relationship betwen A and
-A:

 - exhaustive: A u -A is always true (EXH)
 - exclusive:  A n -A is always false (EXC)

Now, asusming that a true proposition is always valid, the EM formula can
be derived from EXH alone:

  true
 ------ (EXH)
 A u -A

The other two relations, however, require EXC.

First, --A => A

Consider EM applied to -A and A (and commutative u):
  -A u --A = true
  -A u A = true

From EXH and EXC we can divide the universe into two mutually exclusive
regions, -A and --A.  Similarly for -A and A.  So A is identical to --A. 
So --A => A.

Second, classical contradiction

 [-A]  -A => B         [-A]  -A => -B
 ------------- (=> E)  --------------
       B                      -B
       ------------------------- (EXC)
                false
             ----------- (=> I)
             -A => false
             ----------- (EXH)
              A => true

So in both cases EXC is required in the argument, but that doesn't appear in

  true
 ------
 A u -A

which only requires EXH.

Note - looking at Wikipedia, it seems that EXC is the "law of
non-contradiction" (LNC).  See also EoP on Dialetheism -
http://plato.stanford.edu/entries/dialetheism/

So presumably intuitionistic logic includes EXC (LNC).  Hence the question.

For 1.8 I think I really need a more detailed intro to logic?  It seems
that there are a bunch of things (like LNC) that I'm not using.

Apparently 1.5 *is* possible.  Rats.

Question 1.7 (correction)

From: "andrew cooke" <andrew@...>

Date: Tue, 31 Jan 2006 17:13:31 -0300 (CLST)

Looking again at my notes, the law of non-contradiction was already
present in the rules (I hesitate to say axioms - I need to go back and see
if any were derived) I had.  In particular (A n -A) => B (! E) seems to be
equivalent.

However, I am still unclear on how I can derive those as a simple process,
line by line, using that forumlation.

Attacking 1.5

From: "andrew cooke" <andrew@...>

Date: Tue, 31 Jan 2006 17:18:01 -0300 (CLST)

I wrote the following to try clarify where I was.  I was also considering
posting it to lambda as a plea for help, but decided it was unsuitable.


I think that my problem is that I am missing an axiom of some kind.  I am
working through http://www.cs.kent.ac.uk/people/staff/sjt/TTFP and you can
see my previous answers at http://www.acooke.org/cute/TTFPExerci1.html. 
Proofs are of the form

Assumptions
----------- (Reason)
Conclusion

And since part of the reason I'm interested in this is that I want to
understand exactly what axioms are assumed, I'm restricting myself to that
approach as much as possible.  Now I have the following transformations
available (ie they are either axiomatic or derived more or less directly
from axioms):


A B           A n B
----- (n I)   ----- (n E)
A n B         A

[A]            A  A => B
:              --------- (=> E)
B              B
------ (=> I)
A => B

A                     [A]    [B]
----- (u I)           :      :
A u B          A u B  C      C
               --------------- (u E)
               C

-A  =  A => ! (defn)    !
(! is bottom)           - (! E / absurdity)
                        A

[A]  [A]         A  -A
:    :           ----- (- E)
B    -B          B
-------- (- I)
-A

So, my basic problem is that I can't see a way to introduce all the
negation present in (A u B) => -(-A n -B)

I can find plenty of proofs of DeMorgan's theorem, but they assume
classical logic (ie they include the law of the excluded middle).  And the
author of TTFP assures me that this proof (in just the one direction)
doesn't require LEM.

As I said, I feel like I'm either missing an axiom or some assumption
(like "-" being distributive or something).  It's also possible I just
don't trust myself enough when manipulating expressions that include !. 
Is it really OK to have ! in the middle of a proof, draw any conclusion,
and for the proof as a whole to be valid?  Presumably ! cannot appear in
the initial assumptions, right?

Question 1.5 (partial)

From: "andrew cooke" <andrew@...>

Date: Tue, 31 Jan 2006 17:40:02 -0300 (CLST)

Prove (A u B) => -(-A n -B)

Rather than derive this directly, it seems that a kind of "truth-table"
approach might work.  However, that raises a pile of questions.  Since
they seem like useful questions anyway, this post...

A   -(-A n -B)
-------------- (=> E)
   -(! n -B)
   --------- (n E)
     -(!)
    ------ (notation)
    ! => !

So assuming A gives something universally (redundantly?) true.  Same for B
and, therefore, for A u B.

Now, is this sufficient?  I can see these possible problems:

(a) The approach above is not constructive and relies on some kind of
"true" value.  However, it doesn't explicitly use the LEM (so it's not
obviously bad either).

(b) The inference from A and B to (A u B) is in words.  I can't see how to
structure the argument starting from (A u B), although I can imagine
writing the B case in parallel (but what then?).  Am I assuming (A n B) =>
(A u B)? Then I would have (A n B) => -(-A n -B) (but maybe that's OK -
see (d)).

(c) How freely can I use ! - is the inference (! n B) => ! OK?

(d) What about the case (-A n -B)?  That is missing from the implicit
"truth table" I had in mind with this approach.  But why do I need to show
this?  I have a gut feeling (no more) that is only necessary with the LEM.
 Certainly => means something weaker than "equivalence".

Question 1.5 (with help)

From: "andrew cooke" <andrew@...>

Date: Wed, 1 Feb 2006 12:34:27 -0300 (CLST)

I ended up asking for help -
http://groups.google.com/group/sci.logic/browse_frm/thread/14d6bae4031f8e0c

Here's the result:

[A u B]2     [-A n -B]1
              --   -- (n E)
              -A   -B
--------------------- (u E)
          !
     -------------- (=> I1)
     (-A n -B) => !
--------------------- (=> I2)
(A u B) => -(-A n -B)

Which seems depressingly trivial in retrospect.

It's probably worth etching the following onto my forehead or something:

  In general, in constructive logic, work on your proof from
  the conclusion to the premises. Look at the main connective
  of your current goal. The introduction rule for the main
  connective should be the last rule you use. Now you have
  one ore more new goals that you need to prove, and possibly
  a few new premisses.

  When your goal has no connective, then you look at the main
  connectives of your current premisses, and use the
  elimination rules to try to prove your goal from them.

  - H. J. Sander Bruggink

Question 1.8

From: "andrew cooke" <andrew@...>

Date: Wed, 1 Feb 2006 16:58:38 -0300 (CLST)

Prove ((A => B) => A) => A using LEM

Using this application of the LEM (X u -X) is "free"

[X => Y]1   X u -X
------------------ (=> E)
      Y u -X
-------------------- (=> I)
(X => Y) => (Y u -X)  (a)

(A => B) => A
-------------  (a, where X = (A => B), Y = A)
A u -(A => B)
-------------  (a, where X = A, Y = B)
A u -(B u -A)
-------------  (DeMorgan; exercise 1.5)
A u (-B n A)
------------  (n E)
  A u A
  -----
    A

So ((A => B) => A) => A

This could be more explicit, I know.  Major thanks to the anonymous
comment on the discussion page at Wikipedia -
http://en.wikipedia.org/wiki/Talk:Peirce%27s_law

Question 1.8 (better reference)

From: "andrew cooke" <andrew@...>

Date: Wed, 1 Feb 2006 17:03:04 -0300 (CLST)

Better URL http://en.wikipedia.org/wiki/Peirce%27s_law (for the "talk"
page click tab at top of screen).

Questions 1.9, 1.10

From: "andrew cooke" <andrew@...>

Date: Wed, 1 Feb 2006 17:34:02 -0300 (CLST)

1.9 "Between every distinct pair of numbers there is a number"

  A x,y . (x != y) E z . ((x < z) n (z < y))


1.10

(a) One-to-one function
  (A x . E y . (f(x) = y)) n (A y . E x . (f(x) = y))

(b) Onto function
  A y . E x . (f(x) = y)

(c) f respects (preserves?) the relation <
  A x,y . (f(x) < f(y) iff x < y)
or
  A x,y . ({(x < y) n (f(y) < f(y))} u -(x < y))

Automated Problem Solving

From: "andrew cooke" <andrew@...>

Date: Sun, 5 Feb 2006 13:22:21 -0300 (CLST)

This may be relevant - http://lambda-the-ultimate.org/node/1285

Questions 1.11, 1.12

From: "andrew cooke" <andrew@...>

Date: Sun, 12 Feb 2006 21:59:26 -0300 (CLST)

[Correction to 10.10 (c):
  A x,y . ({(x < y) n (f(x) < f(y))} u {-(x < y) n -(f(x) < f(y))}) ]


10.11 In
  A x . {(x < y) n (A z . (y > z => E x . (x > z)))}
    1     1   f       3    f   3      2    2   3

  y is free (f)
  x is bound (twice, 1 and 2)
  z is bound (once, 3)


10.12 Rename z to y in
  A z . E y . (z < y n y < z)

y is already bound, so need to rename y to x (say):
  A z . E y . (z < y n y < z) [y/z]
    = A z . E y . (z < y n y < z) [x/y][y/z]
    = A z . E x . (z < x n x < z) [y/z]
    = A y . E x . (y < x n x < y)

Summary of New (Predicate) Rules

From: "andrew cooke" <andrew@...>

Date: Sun, 12 Feb 2006 22:13:50 -0300 (CLST)

B
------- (A I) side condition: x not free in any assumption of B
A x . B

A x . B(x)
---------- (A E)
B(t)                               [B]
                                   :
B(t)                     E x . B   C
---------- (E I)         ----------- (E I)
E x . B(x)               C

Correction and Clarification

From: "andrew cooke" <andrew@...>

Date: Mon, 13 Feb 2006 10:49:28 -0300 (CLST)

Correction - last rule above is (E E) (ie existential elimintion).

Clarification - on page 25 the book says:

  If we adopt a backwards reading of the rule of existential
  elimination, then we see how to use an existential assumption.

  To use an existential assumption Ex.P(x) , use the instance
  P(x) and finally discharge this using the rule (E E).

What it's saying is: if you need to prove something with an existential
assumption, first start without it, using the unqualified formula.  Later,
introduce the existenctial assumption it as a *separate* assumption, via E
E, which eliminates the initial unqualified formula, leaving the qualified
one (which in turn, is used, typically by => I).

Question 1.13

From: "andrew cooke" <andrew@...>

Date: Mon, 13 Feb 2006 15:06:38 -0300 (CLST)

[Note that "A" and "E" are "ForAll" and "Exists", so I'm rewriting
functions from the text with different letters identifying formulae to
avoid A]

Given the valid proof of Ey.Ax.B(x,y) => Ax.Ey.B(x,y):

[Ax.B(x,y)] (1)
----------- (A E)
  B(x,y)
 --------- (E I)
 Ey.B(x,y)
------------ (A I) (*)
Ax.Ey.B(x,y)          [Ey.Ax.B(x,y)] (2)
------------------------------------ (E E (1))
          Ax.Ey.B(x,y)
---------------------------- (=> I (2))
Ey.Ax.B(x,y) => Ax.Ey.B(x,y)

Note that at (*) x is not free in the assumptions (it is bound by the
for-all clause).

For the corresponding proof of Ax.Ey.B(x,y) => Ey.Ax.B(x,y:

[B(x,y)] (1)
--------- (A I !!!) (**)
Ax.B(x,y)               [Ax.Ey.B(x,y)] (2)
------------ (E I)      -------------- (A E)
Ey.Ax.B(x,y)               Ey.B(x,y)
------------------------------------ (E E (1))
            Ey.Ax.B(x,y)
---------------------------- (=> I (2))
Ax.Ey.B(x,y) => Ey.Ax.B(x,y)

the step (**) is invalid because x is free in the initial assumption. 
This is the "side condition" referenced in the question.

Comment on this post