Diary: programming is hard!

I remember a post by James Thompson (can't find it - sorry) describing the joy of giving IQ tests to bright students. Their smug condescension as they breeze through the early items; their horror as they hit their cognitive limits and start to sweat: "Wait a mo, .., just can't seem to see it ... ."

In artificial intelligence textbooks it's standard to cover the coding of theorem provers for propositional-calculus. Hidden away in the advanced exercises is the suggestion to extend the program to cover the full predicate-calculus. Inevitably, this is flagged as hard.

Tell me about it. Today I got basic binary resolution to work. Great! I can do inference. And yet this is not the central mystery of a predicate-calculus resolution theorem prover (RTP).

The conceptual problems arise from the layers of abstraction around the proof procedure. At the risk of boring you even further, binary resolution is driven by the unification of complementary literals (basic formulae). These two literals occur in the two clauses offered to the resolution function (hence binary resolution).

A  problem addressed by an RTP comprises: assumptions  = the axioms, a set of clauses, plus the problem itself, a goal clause.

Here's my working example. First come the axiom clauses:

(defvar *c3*   (mk-fact-clause '(likes rod horvath)))
(defvar *c4*   (mk-fact-clause '(likes sally renner)))
(defvar *c5*   (mk-fact-clause '(likes sally rod)))
(defvar *c6*   (mk-fact-clause '(likes hardy renner)))
(defvar *c7*   (mk-fact-clause '(likes hardy rod)))
(defvar *c8*   (mk-fact-clause '(amusing hardy)))
(defvar *c9*   (mk-fact-clause '(likes horvath moties)))
(defvar *c10* (mk-rule-clause '(likes sally ?x) '((likes ?x moties)) ) )
(defvar *c11* (mk-rule-clause '(likes rod ?x) '((likes ?x renner) (likes ?x rod)) ) )
(defvar *c12* (mk-rule-clause '(likes ?x ?y) '((amusing ?y) (likes rod ?y)) ) )
(defvar *c13* (mk-fact-clause '(likes ?x ?x)))

(defvar *g1* (mk-goal-clause '((likes sally ?who)) ) )  ; this is the problem clause

You may notice a "Mote in God's Eye" theme here.

Despite the simplicity of these facts and rules, you'll struggle a bit to figure out the complete list of who, exactly, Sally Fowler likes.

I expect better from my program - once completed.

---

So a clause might look like this (which you will recognise as a Prolog-style Horn-clause):

'( (likes sally ?x) ← ((likes ?x ?y) (likes ?y moties)) )   ; a rule clause

which is already a bit complicated.

Then we have to set up structures for the knowledge-base (facts and rules), the goals which emerge from the resolution process, and the pointers and bindings which allow a reconstruction of proofs.

---

In telling you this, my intention is not to document the program, my point is more psychological.

You need to keep a very great deal of abstract structure in your head simultaneously if you hope to put this not-entirely-trivial program together. Plus lots of functions.

It's very g-loaded, much like doing mathematics.

"It's quite hard getting figures but ... it appears that the average IQ of students applying for PhD programmes at good universities in computer science is around 128.

"That sounds right to me. Most software development companies don't take people without good first degrees or a higher degree in a STEM subject - and that's just the pool we're talking about here."

---

Parenthetically, thank God for Lisp, a gift from the deity for clear, conceptual, exploratory thinking.

---

I read endless texts in the media from innumerate journalists about how unemployed or newly-redundant workers are going to retrain as software developers. Those writers couldn't hack it themselves and sadly, neither will most of those no-longer-required workers.

"Wait a mo, ..., just can't seem to see it ... ."

At an IQ threshold of 128, we're talking about 2.5% of a population normed at 100.

A caveat. It's intellectually hard writing machine learning programs or configuring recalcitrant artificial neural nets on novel problem-domains .. or programming RTPs. Yet for everyone doing those things, there are ten people paid to use graphical web design tools or load databases, or do a bit of scripting. Things which are not that hard.

Like many occupations, there has been mission-creep in the definition of software developer.

---

And why am I making such heavy weather of this wretched theorem-prover? This.