From a4c2453f48a38f05aa372d77181dc31a9482fda8 Mon Sep 17 00:00:00 2001 From: Peter Kourzanov Date: Wed, 5 Nov 2014 18:15:43 +0100 Subject: [PATCH] updated with comments --- recette/memo.scm | 63 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 53 insertions(+), 10 deletions(-) diff --git a/recette/memo.scm b/recette/memo.scm index 09c0d27..323b3c0 100644 --- a/recette/memo.scm +++ b/recette/memo.scm @@ -1,3 +1,12 @@ +;; show that tabled miniKanren relations can solve the left-recursion elimination. +;; the grammar can be either CFG or Left-regular and is encoded using Prolog's DCGs +;; based on the difference list technique (code was originally auto-generated). +;; +;; If the top-level goal (X) is not tabled then the program diverges (under both +;; the interpreter and the compiler, obviously). We are using Bigloo 4.1a on 64-bit Ubuntu here. +;; +;; Peter Kourzanov + (module Parse-memo (library bkanren srfi1 slib) ) @@ -28,6 +37,9 @@ ))) )) +;; some preliminaries... + +;; tabled [[appendo]] (define tappendo (tabled (a b c) (tconde ([t== a '()] (t== b c)) @@ -45,7 +57,13 @@ (trun 2 (q) (exist (x y) (tappendo x '(c) y) (t== q `(,x ,y)))) (trun* (q) (exist (x y) (tappendo '(a b) x y) (t== q `(,x ,y)))) -;(exit) + +;; our test grammar (can be CFG, but now is Left-regular) +;; X=z|X a +;; uncomment the (t== Lin (cons 'b temp)) below to make it +;; X=z|b X a +;; the output of the goal is a Peano representation of n in: +;; X=L={a^n b^n|n>=0} (define head_75 (lambda (Lin Lout var) @@ -58,15 +76,20 @@ (define head_77 (lambda (Lin Lout var) - (exist (x temp) + (exist (x temp temp1) (t== var (list 'S x)) - (X Lin temp x) - (t== temp (cons 'a Lout)) + ; although this could be CFG, can show left-recursion problem + ; with a left-regular language (therefore, don't match 'b) + (t== Lin temp) + ;(t== Lin (cons 'b temp)) + (X temp temp1 x) + (t== temp1 (cons 'a Lout)) ) )) (define X +;; exchange [[lambda]] for [[tabled]] to see divergence (tabled args (tconde (tfail) ((apply head_75 args)) @@ -75,6 +98,31 @@ )) +;; swap these branches if you exchanged CFG <=> Left-regular +(if #f (begin +(verify SS.zero (trun* (q) (X '() '() q)) ===> z) +(verify SS.fwd1 (trun* (q) (X '(b a) '() q)) ===> (S z)) +(verify SS.fwd2 (trun* (q) (X '(b b a a) '() q)) ===> (S (S z))) +(verify SS.prefix (trun* (q) (exist (_ r) (X '(b b b a a a) _ r) (t== q `(,_ ,r)))) ---> + ((b b b a a a) z) + (() (S (S (S z)))) + ) +(verify SS.rev0 (trun* (q) (X q '() 'z)) ===> ()) +(verify SS.rev1 (trun* (q) (X q '() '(S z))) ===> (b a)) +(verify SS.rev2 (trun* (q) (X q '() '(S (S z)))) ===> (b b a a)) +(verify SS.fail (trun* (q) (X '(a) '() q)) =>) +(verify SS.fail (trun* (q) (X '(a a) '() q)) =>) +(verify SS.fail (trun* (q) (X '(a a a) '() q)) =>) +(verify SS.fail (trun* (q) (X q '() 'x)) =>) +(verify SS.fail (trun* (q) (X q '() '(S x))) =>) +(verify SS.fail (trun* (q) (X q '() '(S (S x)))) =>) +(verify SS.enum (trun 3 (q) (exist (x y) (X x '() y) (t== q `(,x ,y)))) ---> + (() z) + ((b a) (S z)) + ((b b a a) (S (S z))) + ) +) +(begin (verify SS.zero (trun* (q) (X '() '() q)) ===> z) (verify SS.fwd (trun* (q) (X '(a a) '() q)) ===> (S (S z))) (verify SS.prefix (trun* (q) (exist (_ r) (X '(a a a a) _ r) (t== q `(,_ ,r)))) ---> @@ -86,11 +134,8 @@ (verify SS.fwd (trun* (q) (X '(a a a a) '() q)) ===> (S (S (S (S z))))) (verify SS.fwd (trun* (q) (X '(a a a a a a) '() q)) ===> (S (S (S (S (S (S z))))))) - (verify SS.rev0 (trun* (q) (X q '() 'z)) ===> ()) (verify SS.rev1 (trun* (q) (X q '() '(S z))) ===> (a)) -;(exit) - (verify SS.rev2 (trun* (q) (X q '() '(S (S z)))) ===> (a a)) (verify SS.fail (trun* (q) (X '(a) '() q)) ===> (S z)) (verify SS.fail (trun* (q) (X '(a a a) '() q)) ===> (S (S (S z)))) @@ -98,7 +143,5 @@ (verify SS.fail (trun* (q) (X q '() 'x)) =>) (verify SS.fail (trun* (q) (X q '() '(S x))) =>) (verify SS.fail (trun* (q) (X q '() '(S (S x)))) =>) - -;(exit) - (verify SS.enum (trun 3 (q) (exist (x y) (X x '() y) (t== q `(,x ,y)))) ---> (() z) ((a) (S z)) ((a a) (S (S z)))) +))