Skip to content

Commit d35ecd7

Browse files
engborisengboris
committed
Update proof-nets examples
1 parent b13376d commit d35ecd7

File tree

3 files changed

+238
-79
lines changed

3 files changed

+238
-79
lines changed

‎examples/proofnets/fomll.sg‎

Lines changed: 4 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
' \________/
4848
'
4949
' then
50-
50+
'
5151
' [3, 6]
5252
'
5353
' This corresponds to the following execution in stellogen
@@ -60,81 +60,7 @@
6060
''' ======================================================== '''
6161
''' SUCCESSFUL TYPING '''
6262
''' ======================================================== '''
63-
' We want to check that we have a proof of identity
64-
' (A ⊗ B) -o (A ⊗ B)
65-
' with the following constellation (two axioms)
63+
' Typing works exactly the same as in examples/proofnets/mll.sg
64+
' with the same specifications (providing you have the right adapters)
65+
' except that the proof of identity (A ⊗ B) -o (A ⊗ B) is
6666
(:= proof? { [+1 +3] [+2 +4]})
67-
68-
' We do it in two steps.
69-
' 1. checking the structure of the candidate
70-
' 2. checking that the duality of variables is coherent
71-
72-
' Specification with tests returning [ok] when interacting
73-
' with a constellation having the shape of a proof of
74-
' (_ ⊗ _) -o (_ ⊗ _)
75-
(spec (-o (⊗ A B) (⊗ C D)) {
76-
[+testrl [
77-
[-A -B +(⊗ A B)]
78-
[-C] [-D +(⅋ C D)]
79-
[-(⊗ A B) +concl] [-(⅋ C D)]
80-
@[-concl ok]]]
81-
[+testrr [
82-
[-A -B +(⊗ A B)]
83-
[-C] [-D +(⅋ C D)]
84-
[-(⊗ A B)] [+concl -(⅋ C D)]
85-
@[-concl ok]]]
86-
[+testll [
87-
[-A -B +(⊗ A B)]
88-
[-D] [-C +(⅋ C D)]
89-
[-(⊗ A B) +concl] [-(⅋ C D)]
90-
@[-concl ok]]]
91-
[+testlr [
92-
[-A -B +(⊗ A B)]
93-
[-D] [-C +(⅋ C D)]
94-
[-(⊗ A B)] [+concl -(⅋ C D)]
95-
@[-concl ok]]]})
96-
97-
' Check if proof? satisfies the test-based specification
98-
'(:: proof? (-o (⊗ 1 2) (⊗ 3 4))
99-
100-
' Check if duality is coherent
101-
' TODO
102-
103-
''' ======================================================== '''
104-
''' FAILING TYPING '''
105-
''' ======================================================== '''
106-
107-
(spec (⊗ A B) {
108-
[-A -B +(⊗ A B)]
109-
@[-(⊗ A B) ok]
110-
})
111-
112-
' To avoid unecessary infinite loop,
113-
' we use a linear type assertion
114-
(macro (::lin Tested Test) (== @(fire #Tested #Test) ok))
115-
116-
(:= proof? [+1 +2])
117-
' (::lin proof? (⊗ 1 2)) ' does not typecheck
118-
119-
''' ======================================================== '''
120-
''' COMPRESSED TESTS '''
121-
''' ======================================================== '''
122-
' Actually, have internal connections which could be compressed
123-
' by pre-executing them, thus avoiding unecessary computation.
124-
' The two specifications above become:
125-
126-
(spec (comp-o (⊗ A B) (⊗ C D)) {
127-
[+testrl [
128-
[-A -B +concl] [-C] [-D]
129-
@[-concl ok]]]
130-
[+testrr [
131-
[-A -B] [-C] [-D +concl]
132-
@[-concl ok]]]
133-
[+testll [
134-
[-A -B +concl] [-D] [-C]
135-
@[-concl ok]]]
136-
[+testlr [
137-
[-A -B] [-D] [-C +concl]
138-
@[-concl ok]]]})
139-
140-
(spec (⊗ A B) @[-A -B ok])

‎examples/proofnets/mll.sg‎

Lines changed: 234 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,234 @@
1+
(use-macros "../milkyway/prelude.sg")
2+
3+
''' ============================================ '''
4+
''' MULTIPLICATIVE LINEAR LOGIC PROOF-STRUCTURES '''
5+
''' ============================================ '''
6+
' MLL proof-structures is a representation of mathematical proofs
7+
' for an elementary fragment of logic dealing with the most
8+
' elementary mechanisms of logical implication.
9+
'
10+
' They are graphs with natural numbers as vertices which are linked
11+
' by the following constructors:
12+
'
13+
' ax
14+
' __ (axiom) (cut)
15+
' / \ \__/
16+
' cut
17+
'
18+
'
19+
' \ / \ /
20+
' ⊗ (tensor) ⅋ (par)
21+
' | |
22+
'
23+
'
24+
' Proof-structures can be executed by a graph-contraction
25+
' procedure called "cut-elimination" using two rules:
26+
'
27+
' ax
28+
' __ 2
29+
' / \__/ ~~ax/cut~~> 1
30+
' 1 cut
31+
'
32+
' contracting two vertices
33+
'
34+
' 1 2 3 4 1 2 3 4
35+
' \ / \ / | | | |
36+
' ⅋ ⊗ ~~⅋/⊗~~> \ \____/__/
37+
' \_____/ \ / cut
38+
' cut \__/
39+
' cut
40+
'
41+
' rewiring the connections upward (left input with
42+
' left input and right with right).
43+
44+
''' ======================================================== '''
45+
''' ENCODING '''
46+
''' ======================================================== '''
47+
' The idea is that an axiom between a and b will be a
48+
' binary positive star:
49+
[(+a X) (+b X)]
50+
51+
' A cut between vertices a and b will be binary negative star:
52+
[(-a X) (-b X)]
53+
54+
' A proof of (a ⅋ b) coming from a proof v is obtained by turning rays
55+
(+a X) (+b X)
56+
' of the constellation corresponding to v into
57+
(+(⅋ a b) [l|X]) (+(⅋ a b) [r|X])
58+
59+
' A proof of (a ⅋ b) coming from proofs va and vb is obtained by turning rays
60+
(+a X)
61+
' of the constellation corresponding to va into
62+
(+(⊗ a b) [l|X])
63+
' and turning rays
64+
(+b X)
65+
' of the constellation corresponding to vb into
66+
(+(⊗ a b) [r|X])
67+
68+
69+
''' ======================================================== '''
70+
''' EXAMPLE '''
71+
''' ======================================================== '''
72+
'
73+
' ax ax ax
74+
' _ __ __
75+
' / \ / \ / \
76+
' 1 2 3 4 5 6
77+
' \ / \ /
78+
' ⅋ ⊗
79+
' |_______|
80+
' cut
81+
82+
' becomes
83+
84+
(:= x {
85+
[(+(⅋ 1 2) [l|X]) (+(⅋ 1 2) [r|X])]
86+
[(+3 X) (+(⊗ 4 5) [l|X])]
87+
[(+(⊗ 4 5) [r|X]) (+6 X)]
88+
[(-(⅋ 1 2) X) (-(⊗ 4 5) X)]
89+
})
90+
91+
' by cut-elimination, it is evaluated into
92+
'
93+
' ax ax ax
94+
' __ __ __
95+
' / \ / \ / \
96+
' 1 2 3 4 5 6
97+
' \ \____/__/
98+
' \ cut/
99+
' \____/
100+
' cut
101+
'
102+
' then
103+
'
104+
' [1, 2] [3, 4] [5, 6]
105+
' \ \______/____/
106+
' \________/
107+
'
108+
' then
109+
'
110+
' [1, 6] [3, 4]
111+
' \ /
112+
' \________/
113+
'
114+
' then
115+
'
116+
' [3, 6]
117+
'
118+
' This corresponds to the following executio in stellogen
119+
' in which [] is a way to initiate a starting point in computation
120+
(:= comp (exec #x @[(-3 X) (+3 X)]))
121+
(:= res { [(+3 X9) (+6 X9)] })
122+
' (== #comp #res)
123+
124+
' as for the proof of identity (A ⊗ B) -o (A ⊗ B):
125+
'
126+
' ax ax
127+
' _ _
128+
' / \ / \
129+
' 1 2 3 4
130+
' \ / \ /
131+
' ⅋ ⊗
132+
' |____|
133+
' cut
134+
'
135+
' it becomes
136+
(:= proof? {
137+
[(+(⅋ 1 2) [l|X]) (+(⊗ 3 4) [l|X])]
138+
[(+(⅋ 1 2) [r|X]) (+(⊗ 3 4) [r|X])]
139+
})
140+
141+
' Actually, all rays could have a unique natural number as head symbol and
142+
' it would still work the same
143+
144+
''' ======================================================== '''
145+
''' SUCCESSFUL TYPING '''
146+
''' ======================================================== '''
147+
' We want to check that we have a proof of identity
148+
' (A ⊗ B) -o (A ⊗ B)
149+
' with the previous constellation
150+
#proof?
151+
152+
' We do it in two steps.
153+
' 1. checking the structure of the candidate
154+
' 2. checking that the duality of variables is coherent
155+
156+
' Specification with tests returning [ok] when interacting
157+
' with a constellation having the shape of a proof of
158+
' (_ ⊗ _) -o (_ ⊗ _)
159+
(spec (-o (⊗ A B) (⊗ C D)) {
160+
[+testrl [
161+
[-(var A) -(var B) +(⊗ A B)]
162+
[-(var C)] [-(var D) +(⅋ C D)]
163+
[-(⊗ A B) +concl] [-(⅋ C D)]
164+
@[-concl ok]]]
165+
[+testrr [
166+
[-(var A) -(var B) +(⊗ A B)]
167+
[-(var C)] [-(var D) +(⅋ C D)]
168+
[-(⊗ A B)] [+concl -(⅋ C D)]
169+
@[-concl ok]]]
170+
[+testll [
171+
[-(var A) -(var B) +(⊗ A B)]
172+
[-(var D)] [-(var C) +(⅋ C D)]
173+
[-(⊗ A B) +concl] [-(⅋ C D)]
174+
@[-concl ok]]]
175+
[+testlr [
176+
[-(var A) -(var B) +(⊗ A B)]
177+
[-(var D)] [-(var C) +(⅋ C D)]
178+
[-(⊗ A B)] [+concl -(⅋ C D)]
179+
@[-concl ok]]]})
180+
181+
' Check if proof? satisfies the test-based specification
182+
(:= adapters {
183+
[(-(⅋ 1 2) [l|X]) +(var 1)]
184+
[(-(⅋ 1 2) [r|X]) +(var 2)]
185+
[(-(⊗ 3 4) [l|X]) +(var 3)]
186+
[(-(⊗ 3 4) [r|X]) +(var 4)]
187+
})
188+
(:= proof?+adapters (exec @#proof? #adapters))
189+
'(:: proof? (-o (⊗ 1 2) (⊗ 3 4))
190+
191+
' Check if duality is coherent
192+
' TODO
193+
194+
''' ======================================================== '''
195+
''' FAILING TYPING '''
196+
''' ======================================================== '''
197+
198+
(spec (⊗ A B) {
199+
[-(var A) -(var B) +(⊗ A B)]
200+
@[-(⊗ A B) ok]
201+
})
202+
203+
' To avoid unecessary infinite loop,
204+
' we use a linear type assertion
205+
(macro (::lin Tested Test) (== @(fire #Tested #Test) ok))
206+
207+
(:= proof? [(+1 X) (+2 X)])
208+
(:= adapters { [(-1 X) +(var 1)] [(-2 X) +(var 2)] })
209+
(:= proof?+adapters (exec @#proof? #adapters))
210+
'(::lin proof?+adapters (⊗ 1 2)) ' does not typecheck
211+
212+
''' ======================================================== '''
213+
''' COMPRESSED TESTS '''
214+
''' ======================================================== '''
215+
' Actually, constellations corresponding to proofs
216+
' have internal connections which could be compressed
217+
' by pre-executing them, thus avoiding unecessary computation.
218+
' The two specifications above become:
219+
220+
(spec (comp-o (⊗ A B) (⊗ C D)) {
221+
[+testrl [
222+
[-(var A) -(var B) +concl] [-(var C)] [-(var D)]
223+
@[-concl ok]]]
224+
[+testrr [
225+
[-(var A) -(var B)] [-(var C)] [-(var D) +concl]
226+
@[-concl ok]]]
227+
[+testll [
228+
[-(var A) -(var B) +concl] [-(var D)] [-(var C)]
229+
@[-concl ok]]]
230+
[+testlr [
231+
[-(var A) -(var B)] [-(var D)] [-(var C +concl)]
232+
@[-concl ok]]]})
233+
234+
(spec (⊗ A B) @[-A -B ok])

‎test/examples.t‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ MALL (multiplicative-additive linear logic) example:
3838

3939
MLL (multiplicative linear logic) example:
4040
$ sgen run ../examples/proofnets/mll.sg
41-
{}
4241

4342
Natural numbers example:
4443
$ sgen run ../examples/nat.sg

0 commit comments

Comments
 (0)