Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace uses of builtin substitution with custom semantics for lambda #3

Merged
merged 10 commits into from
Jan 30, 2024
Merged

Replace uses of builtin substitution with custom semantics for lambda #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
41b5f1b
Replace uses of the substitution module
gtrepta Jan 18, 2024
61faa98
Alpha conversion for lesson 2
gtrepta Jan 29, 2024
4607c4a
Alpha conversion for lesson 2.5
gtrepta Jan 29, 2024
8d6dc89
Alpha conversion for lesson 3
gtrepta Jan 29, 2024
0ebf254
Alpha conversion for lesson 4
gtrepta Jan 29, 2024
339ba3d
Alpha conversion for lesson 5
gtrepta Jan 29, 2024
7ec6351
Alpha conversion for lesson 6
gtrepta Jan 29, 2024
3a225c1
Alpha conversion for lesson 7
gtrepta Jan 29, 2024
e99f658
Alpha conversion for lesson 8
gtrepta Jan 29, 2024
fce0036
Alpha conversion for lesson 9
gtrepta Jan 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 25 additions & 7 deletions 1_k/1_lambda/lesson_2.5/lambda.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
32 changes: 25 additions & 7 deletions 1_k/1_lambda/lesson_2/lambda.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<k>
lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
</k>
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<k>
a ( ( lambda x . lambda y . x ) y0 z ) ~> .
a ( ( lambda x . lambda y . x ) y z ) ~> .
</k>
32 changes: 25 additions & 7 deletions 1_k/1_lambda/lesson_3/lambda.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<k>
lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
</k>
32 changes: 25 additions & 7 deletions 1_k/1_lambda/lesson_4/lambda.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<k>
lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
</k>
41 changes: 34 additions & 7 deletions 1_k/1_lambda/lesson_5/lambda.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<k>
lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
</k>
44 changes: 37 additions & 7 deletions 1_k/1_lambda/lesson_6/lambda.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion 1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<k>
lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
</k>
Loading