THORN 20: procedural attachment

[dr.mt...@gmail.com]

The limits of inference for this architecture w.o. major additions were reached in THORN 19.  But one change actually makes THORN 19 much more useful and that is procedural attachment.  This is easily effected in less than 10 lines.

Procedural attachment is a feature in theorem-provers going way back.  For example, given as the goal 3 < 10, it is obvious that the native arithmetic engine needs to be called to prove this, not the inference engine itself.  Procedural attachment is also a feature of Prolog.

In THORN 20, the higher-order call predicate in Shen Prolog can be invoked.  For example in my Tarski-flavoured semantics I had an axiom.

      [all x [all y [all z [[[name x] & [[copEng y] & [adjEng z]]]
      <=> [[istrueEng [cn x [cn y z]]] <=> [sat [den x] z]]]]]]

and 

[adjEng "bald"]

But if I were to expand this system to incorporate thousands of English adjectives, I 'd have thousands of atomic statements in my axiom base.  It would probably not compile; imagine a function def of adjEng with > 1 million loc!!

The solution is procedural attachment; I replace the axiom in red by

[all x [[call [adjEng? x]] => [adjEng x]]]  

and add

(defprolog adjEng?
  X <-- (when (element? X (value *EngAdj*)));) 

(set *EngAdj* ["bald" ....])

call, as you might know, figures in Shen Prolog.  It calls a Prolog goal.

(prolog? (call (is X a)))

true

In THORN it is embedded in a way to preserve the syntax of the type prop.

The called procedure has access to resources from THORN; they are kept in the variables Prf, Max, Depth, Hyp.  The most useful is the variable Hyp, which codes the hypotheses available at that stage of the proof.  We can do stuff like this.

(define mytypechecking
  {--> (list prop)}
   -> [[all x [all type [[call [typecheck! x type (protect Hyp)]]

                         => [x : type]]]]])

(defprolog typecheck!
   X Type Hyp <-- (shen.system-S-h X Type Hyp);)  

(kb-> (mytypechecking))
compiled

(<-kb [4 : number])

run time: 0.015625 secs
44 inferences, equality = false
depth = 20, complexity = -1, timeout = 60 secs
true

So you can link the type system into THORN.  And that means, should you want to explore some exotic verification system or type theory, run under first-order logic  and call on the Shen type system, you can do it.

One last caveat, call expects to know the arity of what it is calling.  This is the higher-order magic behind the totally laconic definition of call in the kernel (the magic for this is in the kernel).

(define call
  Call Bindings Lock Key Continuation 

     -> (Call Bindings Lock Key Continuation))

So I use typecheck! to meet that need.  THORN 20 will go up soon.

Mark