LKL - Logic for KLambda

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

Quite often with code, I'll prototype ideas and develop them and leave them for years, only to return to them later.  In the meantime some part of the brain seems to have been working on them.    This process of refinement led to the first S series kernel in 2019 and here I have returned to the theme of the formal verification of Shen programs.

Formal specification and verification is more talked about than implemented; for the very good reason that formal verification is very arduous.  My initial experiments with LKL showed that even 'simple' proofs like the associativity of append would take over 60 steps to produce.  This is very usual and led Milner et al.  to experiment with tactics which are discussed in Lecture 21 of Logic, Proof and Computation.  But even tactics fall short and sometimes automatic theorem provers can make life easier.  60+ steps can be reduced to 4 with this method.

In this case, to work with LKL, the theorem prover needs to borrow on the inferential power of the Shen type checker combining this with inferencing for first-order logic with equality (LKL is actually second order but most problems are first-order).  I've forked off a version of THORN - THORN-LKL which I will test in this role.  Equality is combinatorially explosive to deal with so I'll reserve verdict on this.   Expect to see later.

Mark

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

One rather radical conclusion I'm coming to is that incorporating types into LKL

not only makes life more complex, but does not actually add very much to the

functionality of the system.   They just amount to a largely futile set of boundary

conditions that you have to get through before the main proof.  Of course, types

are useful in programming, but oddly not that much use in formal verification apparently.

So I'm going to produce LKL without types and see how that flies.   

Mark