This tutorial is presented below as Shen source, so that it may be interactively evaluated.
\* Shen Tutorial: Sequent Calculus *\
\* I. Background Shen’s sequent calculus is a Turing-complete language for logical proof and computation. When employed in the domain of type checking, it provides extra power and convenience compared to the underlying Horn clause logic (Prolog) of which it is implemented. Sequent calculus has its origins in proof theory and mathematical logic. A computer programmer, if having no prior experience with it in mathematics, may find it easier to ignore the formal expositions and concentrate on how this particular variety of the notation translates into Shen Prolog. Basic understanding of Shen Prolog is assumed. It may also be helpful to disregard notions of left and right rules, since they have no relevance from an operational standpoint. *\
\* II. T* The internal function shen.t* is the top level implementation of the type checking algorithm. Its parameters are an expression to type check and an assumption context. Assumptions will be discussed later - the context can be assumed to be an empty list for now. The expression in the first parameter has two different input formats. The first format contains a top level type annotation and the second does not. In the case of the first format only, the expression is expected to have all its function applications in curried form (unless the function is flagged ‘special’ - see the Shen system function ‘specialise’). *\
(package null []
(prolog? (shen.t* [[+ 1 2] : T] []) (return T)) \\ false - not curried
(prolog? (shen.t* [[[+ 1] 2] : T] []) (return T)) \\ number
)
\* III. Syntax There are two different categories of expressions - those with type annotations and those without. Each expression category has slightly different unification and compilation semantics. *\
(package null []
\* 1. Basic Expressions We begin with an example using clauses which contain no type annotations. *\
(datatype m0-basic
Body1;
BodyN;
\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
Head;)
\* The horizontal line is referred to as the inference line. It separates the pattern matching head of a clause from its body. If during the type checking process an expression matches the head of a clause, the rule fires. The body clauses are then tested in turn. The flow of execution can therefore be read bottom up. When type checking, all generated datatype functions are called in the reverse order of their definition. This effectively merges all definitions into a single function for type checking all expressions. The above (useless and non-terminating) datatype definition translates in to the Prolog function below. *\
(defprolog type#m0-basic Head Context <– (shen.t* Body1 Context) (shen.t* BodyN Context);)
\* The definition loops forever because the head matches everything, and the tests in the body indirectly trigger self recursion. *\
(prolog? (shen.t* Head [])) \\ maximum inferences exceeded (preclude [m0-basic])
\* 2. Annotated Expressions The second example contains type annotations. Note how the pattern matching and unification mode declarations are different in the Prolog output compared to the previous example. *\
(datatype m1-basic
Body : T;
\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
Head : any;)
(defprolog type#m1-basic (mode [Head : (mode any +)] -) Context <– (shen.t* [Body : T] Context);)
(prolog? (shen.t* Head [])) \\ false, since we deleted the m0-basic rule (prolog? (shen.t* [Head : any] [])) \\ maximum inferences exceeded
(preclude [m1-basic]) )
\* IV. Assumption Context The assumption context is an arbitrary set of facts which may be used to assist the proof. Facts may be produced and consumed in different contexts as the proof proceeds. A sequent clause may depend on a certain fact being in the current context before firing, and it may also introduce new facts when proving clauses in its body. Assumptions are typically introduced by ‘let’, ‘lambda’, and ‘define’ to describe the variables they introduce. Syntactically, assumptions are both consumed and produced using the » operator. The behavior varies based on if it is used below or above the inference line. The left side of the operator contains one or more comma separated assumptions, while the right side is the expression that is to be proved. Below the inference line, assumptions indicate additional facts which must exist in a given context before the rule is allowed to fire. If a match occurs, the fact is removed from the current context when evaluating the clauses above the inference line. Above the inference line, assumptions indicate additional facts which are to be added to the current context before type checking the expression to the right. The flow of execution in a sequent can therefore be followed clockwise from the bottom-right like so: 3 » 4 _____________ 2 » 1 If expression 1 is matched and expression 2 is found in the context, then expression 2 is removed from the context. Expression 3 is then added to the remaining context while verifying expression 4. The first example below shows how a second support routine is generated to match and discard the given assumption from the context before proceeding *\
(package null []
(datatype a-basic
dog, cat \>> P;
\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
fact \>> P;)
(defprolog type#a-basic P Context <– (shen.cl11910 Context Context1) (bind ContextOut Context1) (shen.t* P [dog cat | ContextOut]);)
(defprolog shen.cl11910 [fact | In] In <–; [X|XS] [X|Out] <– (shen.cl11910 XS Out);)
(preclude [a-basic]) )
\* V. Extra Syntax Certain extra syntax, unrelated to sequent calculus, is allowed to appear before the first clause in the body. ‘if’ and ‘let’ are equivalent to ‘is’ and ‘when’ in Shen Prolog. *\
(datatype extra-if-let-cut
if (\= true true)
let Y "abc"
!; Z;
\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
X; )
(defprolog type#extra-if-let X Context <– (when (= true true)) (is Y “abc”) ! (shen.t* Z Context);)
(preclude [extra-if-let-cut])
\* Note that variables assigned by let bindings do not directly unify with the right hand side of a type annotation, due to the way ‘is’ works. An extra unification step is needed. *\
(datatype unify-something
let Y (some test)
(Z ~ Y);
\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
(expr X) : Z;
\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_
(X ~ X);)
(preclude [unify-something])
\* VI. Verified Types As hinted before, ‘define’ introduces extra assumptions to the context before type checking its body. In addition to type information, regarding both the function itself and its parameters, it will also add so-called verified types generated by guard conditions. In the below function, when trying to prove: ____________ 7 : number The assumption context will be: 1. (integer? &&X) : verified 2. &&X : number 3. verified-test : (number –> number) The type system can therefore assume things based on the presence of run-time checks. *\
(define verified-test { number --> number } X -> 7 where (integer? X) X -> 0)
\* VII. Debug The prolog definitions shown in this document were ported from the Horn clauses generated by Shen’s internal compilation routines. They may be traced with the following hooks: *\
(set debug.*datatype* true)
(define datatype.trace Msg X -> (if (value debug.*datatype*) (do (output “~A:~%~R~%” Msg X) X) X))
(define shen.process-datatype D Rules -> (let Clauses (shen.rules->horn-clauses D Rules) Compiled (shen.s-prolog (datatype.trace “datatype.main” Clauses)) (shen.remember-datatype Compiled)))
(define shen.construct-search-clause Pred A V -> (let Clauses [(shen.construct-base-search-clause Pred A V) (shen.construct-recursive-search-clause Pred A V)]
(shen.s-prolog
(datatype.trace "datatype.search" Clauses))))