Logic Lab

[Mark Tarver]

This tech will be released this year as part of the Logic Lab with a monograph
of around 100 pages to go in the coffee and donut report Shen series.  It enables
the formal verification of any Shen program and is based on an axiomatic semantics
for KLambda which translates Klambda into a second-order logic LKL.

Addition over natural numbers is defined as

(define add
    0 N -> N

    M N -> (succ (add (pred M) N)))

A formal proof of the associativity of this addition function opens

=========================
Step 0 [1]

?- [all x
 [all y
  [all z
   [
    [add x
     [add y z]] =
    [add
     [add x y] z]]]]]
 
> mathind  (introduce math'l induction as an axiom)

and ends

Step 117 [1]

?- [
 [add tm0
  [add tm1 tm2]] =
 [add
  [add tm0 tm1] tm2]]

1. [
 [add tm0
  [add tm1 tm2]] =
 [add
  [add tm0 tm1] tm2]]
 
> hyp

true : boolean

Note after step 3 the proof is first-order.

I'm going to connect this system to Prover9 - a powerful system for first-order logic.
99% of the proofs in LKL are first-order after induction is performed so great savings are
possible.

Anybody interested in testing this out when done can reply here.

Mark

[Mark Tarver]

Well seemingly I've cracked the axiomatic semantics for KLambda - about the hardest thing I've done in many moons.   It requires some quite clever logical techniques to do this and I've written it up in about 100 sides.

Other stuff is on the backplate as I finish this.

The logic transformations take 550 lines of code to map KLambda into 2nd order logic.  The most important aspect is that the transformations are provably sound.  

Mark

[Mark Tarver]

I've actually done this before but in a different way and not provably sound and not from KLambda as the source.  Here FYI is a chunk of kernel code and the axioms therefrom.

(define append
  [] X -> X
  [X | Y] Z -> [X | (append Y Z)]
  _ _ -> (simple-error "attempt to append a non-list"))

(define boolean?
  true -> true
  false -> true
  _ -> false)

(define difference
  [] _ -> []
  [X | Y] Z -> (if (element? X Z) (difference Y Z) [X | (difference Y Z)])
  _ _ -> (error "attempt to find the difference with a non-list~%"))

(define do
  X Y -> Y)

(define element?
  _ [] -> false
  X [X | _] -> true
  X [_ | Z] -> (element? X Z)
  _ _ -> (error "attempt to find an element in a non-list~%"))

(all x ((append () x) = x))
(all x (all y (all z ((append (cons x y) z) = (cons x (append y z))))))
(all x (all y (((~ (() = x)) & (all xn (all yn (~ (x = (cons xn yn)))))) => ((append x y) = (abort)))))

((boolean? true) = true)
((boolean? false) = true)
(all x (((~ (true = x)) & (~ (false = x))) => ((boolean? x) = false)))

(all x ((difference () x) = ()))
(all x (all y (all z (((element? x z) = true) => ((difference (cons x y) z) = (difference y z))))))
(all x (all y (all z (((element? x z) = false) => ((difference (cons x y) z) = (cons x (difference y z)))))))
(all x (all y (((~ (() = x)) & (all xn (all yn (~ (x = (cons xn yn)))))) => ((difference x y) = (abort)))))

(all x (all y ((do x y) = y)))

(all x ((element? x ()) = false))
(all x (all y ((element? x (cons x y)) = true)))
(all x (all y (all z ((~ (y = x)) => ((element? y (cons x z)) = (element? y z))))))
(all x (all y (((~ (() = y)) & (all xn (all yn (~ (y = (cons xn yn)))))) => ((element? x y) = (abort)))))

One interesting aspect is that the techniques used can be used on pretty much any member of the Lisp family with a little adaptation.

Mark