Logic Lab write up

[Mark Tarver]

I'm writing up the Logic Lab which may turn out to be a second course  building on Logic, Proof and Computation.    My focus however is not on teaching first-order logic and the philosophy of logic (as in  Logic, Proof and Computation  which was part of a first year course) but in teaching people how to build their own type secure logical systems in Shen.  In the course of this, I will explore a number of systems.

The Logic Lab is really a reanimation of some older work.

SEQUEL (SEQUEnt processing Language) was the ancestor of Shen and was introduced in 1992 in The Sixth International Conference on Symbolic and Logical Computing.  SEQUEL was designed from the outset as a shell in which logic rules could be entered directly as sequent rules.  Unlike the LCF and the LF, SEQUEL was a programming language in its own right; sequent rules were used to describe type theories which were used to typecheck SEQUEL programs.   

SEQUEL was to evolve into Qi in 2005 which became Shen in 2011.   The essential ideas remained the same, though the realisation of those ideas became steadily more sophisticated over a 30 year period.  During that period, the focus of direction for SEQUEL/Qi/Shen moved from representing logics to programming in general and Qi was even used to model transport systems.  

By the time of Shen, the focus was entirely on general purpose programming.  In this respect, Shen followed the trajectory of ML, which began life as a support language for programming proof strategies in the LCF and ended as a general purpose programming language in the shape of Standard ML.

Qi, introduced in 2005 and published in 2008 was the last version of my work to include inbuilt provision for the representation of arbitrary logical systems and an inbuilt proof assistant for executing proofs.   In 2011 Shen left this feature completely behind.  

In 2021 I began to reflect that this application area should be brought back by some form of library code.  Thus was born the Logic Lab, which combined the modern resources of Shen with the ability to frame logical systems directly in terms of sequent rules.  The Logic Lab benefited greatly from the 30 year gap between SEQUEL and the latest S30 Shen kernel that I was using in 2021.   

Not only does the Logic Lab generate highly efficient code from sequent calculus, but this code is automatically proved to be type secure wrt the syntax of the logic in question.  The Logic Lab also solves certain awkward questions (that I had not solved in 1992) about formalising sequent rules with unusual side conditions (we'll see some of those later) and best of all – it doesd all this in less than 500 lines of Shen!

Mark

[Mark Tarver]

The Time New Roman text is taken directly from my write up.

Mark

[Bruno Deferrari]

Mark, is this going to be a book, a course, documentation in SP or what?

> --
> You received this message because you are subscribed to the Google Groups "Shen" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/166bbee5-4dee-48c0-8bf7-3c85292e7176n%40googlegroups.com.



--
BD

[Mark Tarver]

I would say a book.  There may be three books concerned with technology that has evolved with SP.

1.  The Logic Lab.

2.  Concurrency.

3.  The Standard Library.

These books will be however much shorter than TBoS which, because of its load bearing role, is necessarily something of a tome.

The books are likely to be monographs of between 100-150 pages and priced correspondingly lower - below the £10 mark.

The Logic Lab book is really a sequel and companion to LPC, but whereas LPC assumes no programming skill and is aimed at 

teaching logic and the philosophy of logic, the Logic Lab book is aimed at people who are interested in fabricating and programming

logical systems.   I aim to study a number of systems whose formalisation is challenging.  I'm covering semantic tableau for FOL

with fully automated reasoning right now.    This is actually a tricky system because one of the inference rules requires referring 

to the entire proof tree (or goal stack if you like).  My aim is to show how this can be done elegantly, type securely and w.o needing

much intellectual baggage and that therefore other logical systems should fall easily to the techniques I'm teaching.

A nice feature of the Logic Lab, unlike Coq et al., is that the sources are really small - around 500 lines.  Small enough to fit into 

appendices and therefore easy to change.

Mark

To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/CACnPB4ou0rc5Q%2B%2Brp0-C8t5kDeBmqpHXWtiV%3DR%2BJpAKkLDmwpQ%40mail.gmail.com.