Chicken Shen

Check-in [f2e10f71e5]
Login
Overview
Comment:Added sequent tutorial in sequent.shen
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA3-256:f2e10f71e575661de9b68c6089097e54850db8c78508b0a0f6342a7798cc27ac
User & Date: david 2019-02-01 10:10:06
Context
2019-02-01
10:10
Added shen code => k-lambda doc check-in: dba3ef221a user: david tags: trunk
10:10
Added sequent tutorial in sequent.shen check-in: f2e10f71e5 user: david tags: trunk
03:04
Updated release-info check-in: 462e8ce86a user: david tags: trunk, v0.1
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Added docs/sequent.shen.





















































































































































































































































































































































































































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
\* 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))))