Update examples (proofnets)

Author: engboris

examples/mll.sg

@@ -0,0 +1,140 @@
+(use-macros "../milkyway/prelude.sg")
+
+''' ======================================================== '''
+''' FIRST-ORDER MULTIPLICATIVE LINEAR LOGIC PROOF-STRUCTURES '''
+''' ======================================================== '''
+' FOMLL proof-structures are MLL proof-structures
+' (cf. examples/proofnets/mll.sg) which contain only cut and axiom
+' constructors.
+'
+' An axiom between vertices x and y becomes the binary postive star
+[+x +y]
+'
+' A cut between vertices y and z becomes the binary negative star
+' which will link two axioms
+[-y -z]
+
+''' ======================================================== '''
+''' FOR EXAMPLE '''
+''' ======================================================== '''
+' MLL proof-structures with only cuts and axioms yield partitions
+' corresponding to axiom links with links between natural numbers.
+'
+'   ax    ax    ax
+'   __    __    __
+'  /  \  /  \  /  \
+'  1  2  3  4  5  6
+'  \   \____/__/
+'   \   cut/
+'    \____/
+'     cut
+'
+'     becomes
+'
+'   [1, 2]  [3, 4]  [5, 6]
+'    \   \______/____/
+'     \________/
+'
+'    corresponding to the constellation
+(:= x {
+  [+1 +2] [+3 +4] [+5 +6]
+      [-1 -4]  [-2 -5]
+})
+'     which evaluates into
+'
+'   [1, 6]  [3, 4]
+'    \          /
+'     \________/
+'
+'    then
+
+'   [3, 6]
+'
+' This corresponds to the following execution in stellogen
+' in which [-3 +3] is a way to initiate a starting point in computation
+(:= comp (exec #x @[-3 +3]))
+(:= res { [+3 +6] })
+(== #comp #res)
+
+
+''' ======================================================== '''
+''' SUCCESSFUL TYPING '''
+''' ======================================================== '''
+' We want to check that we have a proof of identity
+' (A ⊗ B) -o (A ⊗ B)
+' with the following constellation (two axioms)
+(:= proof? { [+1 +3] [+2 +4]})
+
+' We do it in two steps.
+' 1. checking the structure of the candidate
+' 2. checking that the duality of variables is coherent
+
+' Specification with tests returning [ok] when interacting
+' with a constellation having the shape of a proof of
+' (_ ⊗ _) -o (_ ⊗ _)
+(spec (-o (⊗ A B) (⊗ C D)) {
+  [+testrl [
+    [-A -B +(⊗ A B)]
+    [-C] [-D +(⅋ C D)]
+    [-(⊗ A B) +concl] [-(⅋ C D)]
+    @[-concl ok]]]
+  [+testrr [
+    [-A -B +(⊗ A B)]
+    [-C] [-D +(⅋ C D)]
+    [-(⊗ A B)] [+concl -(⅋ C D)]
+    @[-concl ok]]]
+  [+testll [
+    [-A -B +(⊗ A B)]
+    [-D] [-C +(⅋ C D)]
+    [-(⊗ A B) +concl] [-(⅋ C D)]
+    @[-concl ok]]]
+  [+testlr [
+    [-A -B +(⊗ A B)]
+    [-D] [-C +(⅋ C D)]
+    [-(⊗ A B)] [+concl -(⅋ C D)]
+    @[-concl ok]]]})
+
+' Check if proof? satisfies the test-based specification
+'(:: proof? (-o (⊗ 1 2) (⊗ 3 4))
+
+' Check if duality is coherent
+' TODO
+
+''' ======================================================== '''
+''' FAILING TYPING '''
+''' ======================================================== '''
+
+(spec (⊗ A B) {
+  [-A -B +(⊗ A B)]
+  @[-(⊗ A B) ok]
+})
+
+' To avoid unecessary infinite loop,
+' we use a linear type assertion
+(macro (::lin Tested Test) (== @(fire #Tested #Test) ok))
+
+(:= proof? [+1 +2])
+' (::lin proof? (⊗ 1 2)) ' does not typecheck
+
+''' ======================================================== '''
+''' COMPRESSED TESTS '''
+''' ======================================================== '''
+' Actually, have internal connections which could be compressed
+' by pre-executing them, thus avoiding unecessary computation.
+' The two specifications above become:
+
+(spec (comp-o (⊗ A B) (⊗ C D)) {
+  [+testrl [
+    [-A -B +concl] [-C] [-D]
+    @[-concl ok]]]
+  [+testrr [
+    [-A -B] [-C] [-D +concl]
+    @[-concl ok]]]
+  [+testll [
+    [-A -B +concl] [-D] [-C]
+    @[-concl ok]]]
+  [+testlr [
+    [-A -B] [-D] [-C +concl]
+    @[-concl ok]]]})
+
+(spec (⊗ A B) @[-A -B ok])

examples/proofnets/fomll.sg

@@ -5,6 +5,7 @@
   (glob_files ./syntax/*.sg)
   (glob_files ./errors/*.sg)
   (glob_files ../examples/*.sg)
+  (glob_files ../examples/proofnets/*.sg)
   (glob_files ../examples/milkyway/*.sg)
   (glob_files ../exercises/solutions/*.sg)
   (package stellogen)))

examples/mall.sg renamed to examples/proofnets/mall.sg

@@ -33,11 +33,11 @@ Linear lambda example:
   {}
 
 MALL (multiplicative-additive linear logic) example:
-  $ sgen run ../examples/mall.sg
+  $ sgen run ../examples/proofnets/mall.sg
   { [(-3 (%cons r (%cons l X4))) (-3 (%cons r (%cons r X4))) || (slice c b)] [(c X11) (d X11) || (slice c a)] }
 
 MLL (multiplicative linear logic) example:
-  $ sgen run ../examples/mll.sg
+  $ sgen run ../examples/proofnets/mll.sg
   {}
 
 Natural numbers example: