Replace uses of builtin substitution with custom semantics for lambda (…

…#3) * Replace uses of the substitution module * Alpha conversion for lesson 2 * Alpha conversion for lesson 2.5 * Alpha conversion for lesson 3 * Alpha conversion for lesson 4 * Alpha conversion for lesson 5 * Alpha conversion for lesson 6 * Alpha conversion for lesson 7 * Alpha conversion for lesson 8 * Alpha conversion for lesson 9
runtimeverification · Jan 30, 2024 · 0eb060b · 0eb060b
1 parent afb72e5
commit 0eb060b
Show file tree

Hide file tree

Showing 18 changed files with 303 additions and 84 deletions.
diff --git a/1_k/1_lambda/lesson_2.5/lambda.k b/1_k/1_lambda/lesson_2.5/lambda.k
@@ -1,21 +1,39 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp
   syntax Exp ::= Val
                | Exp Exp              [left]
                | "(" Exp ")"          [bracket]
 endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]   [anywhere]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]   [anywhere]
 endmodule
diff --git a/1_k/1_lambda/lesson_2/lambda.k b/1_k/1_lambda/lesson_2/lambda.k
@@ -1,21 +1,39 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp
   syntax Exp ::= Val
                | Exp Exp              [left]
                | "(" Exp ")"          [bracket]
 endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 endmodule
diff --git a/1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out b/1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  a ( ( lambda x . lambda y . x ) y0 z ) ~> .
+  a ( ( lambda x . lambda y . x ) y z ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_3/lambda.k b/1_k/1_lambda/lesson_3/lambda.k
@@ -1,23 +1,41 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
 endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 endmodule
diff --git a/1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_4/lambda.k b/1_k/1_lambda/lesson_4/lambda.k
@@ -1,23 +1,41 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
 endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 endmodule
diff --git a/1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_5/lambda.k b/1_k/1_lambda/lesson_5/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -22,12 +20,41 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 
   rule - I => 0 -Int I
   rule I1 * I2 => I1 *Int I2

diff --git a/1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_6/lambda.k b/1_k/1_lambda/lesson_6/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -24,12 +22,44 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+  rule freeVars( if B then E1 else E2) => freeVars(B) freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
+  rule (if C then E1 else E2) [V / X] => if C[V / X] then E1[V / X] else (E2[V / X])
+
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 
   rule - I => 0 -Int I
   rule I1 * I2 => I1 *Int I2

diff --git a/1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>