Formal Model¶

Environment¶

Environment (Γ) maps names to values:

# Environment example:
# Γ = {x: 42, y: "hello", z: [1, 2, 3]}

x = 42
y = "hello"
z = [1, 2, 3]

Formal notation:

Γ[x ↦ v]  # Bind x to value v in Γ
Γ(x)      # Lookup x in Γ

# Before: Γ = {}
x = 42
# After: Γ = {x: 42}

# Before: Γ = {x: 42}
y = "hello"
# After: Γ = {x: 42, y: "hello"}

# Before: Γ = {x: 42}
x = 100
# After: Γ = {x: 100}

Γ ⊢ e ⇓ v

Means: "In environment Γ, expression e evaluates to value v"

# Γ = {x: 10, y: 20}
# Γ ⊢ x + y ⇓ 30

x = 10
y = 20
result = x + y  # 30

# Global: Γ_global = {x: 10}
x = 10

def f():
    # Local: Γ_local = {y: 20}
    # Parent: Γ_global
    y = 20
    return x + y

Γ_local → Γ_enclosing → Γ_global → Γ_builtin

# Γ ⊢ x = e ⇓ Γ[x ↦ v]
# where Γ ⊢ e ⇓ v

x = 42
# Evaluates 42, binds x

# Γ ⊢ x, y = e1, e2 ⇓ Γ[x ↦ v1, y ↦ v2]

x, y = 1, 2

def f(x, y):
    return x + y

# Call: f(10, 20)
# Creates: Γ_f = Γ_global[x ↦ 10, y ↦ 20]

Γ ⊢ f(e1, e2) ⇓ v
where:
  Γ ⊢ e1 ⇓ v1
  Γ ⊢ e2 ⇓ v2
  Γ' = Γ[x ↦ v1, y ↦ v2]
  Γ' ⊢ body ⇓ v