Formal Semantics — ভাষার অর্থ গণিতে লেখা

নতুন construct:

e ::= ... | let x = e₁ in e₂

মানে: environment-এ x := e₁-র মান bind করে e₂ হিসাব করো। দুই evaluator-এ দুই ভিন্ন কৌশল লাগবে — আর সেই পার্থক্যটাই শিক্ষণীয়।

def let(x, bound, body):
    return ('let', x, bound, body)

# ── Big-step: environment extend করে (dynamic approach) ──────
def big_step_v2(e, env=None):
    env = {} if env is None else env
    tag = e[0]
    if tag == 'let':
        v = big_step_v2(e[2], env)              # B-Let premise ১: e₁ ⇓ v₁
        return big_step_v2(e[3], {**env, e[1]: v})  # premise ২: নতুন ρ-তে e₂
    # ... বাকি cases আগের big_step-এর মতোই
    return big_step(e, env)

# ── Small-step: substitution দিয়ে (static approach) ──────────
def subst(e, x, val):
    """e-র ভেতরে ('var', x)-এর সব occurrence-এর জায়গায় val বসাও"""
    tag = e[0]
    if tag == 'num':  return e
    if tag == 'var':  return val if e[1] == x else e
    if tag in ('add', 'mul'):
        return (tag, subst(e[1], x, val), subst(e[2], x, val))
    if tag == 'if0':
        return ('if0', subst(e[1], x, val),
                       subst(e[2], x, val), subst(e[3], x, val))
    if tag == 'let':
        _, y, bound, body = e
        if y == x:                              # ভেতরের let একই নাম —
            return ('let', y, subst(bound, x, val), body)  # shadowing: ভেতরের body স্পর্শ নয়
        return ('let', y, subst(bound, x, val),
                       subst(body, x, val))
    raise ValueError(tag)
def step_v2(e):
    tag = e[0]
    if tag == 'let':
        _, x, bound, body = e
        if not is_value(bound):
            return ('let', x, step_v2(bound), body)   # S-Let-Bound
        return subst(body, x, bound)                  # S-Let: substitute
    # ... বাকি cases আগের step-এর মতোই
    return step(e)

# ── pretty-printer: let সহ (experiment-এর show-এর extension) ──
def show_v2(e):
    tag = e[0]
    if tag == 'num':
        return str(e[1])
    if tag == 'var':
        return e[1]
    if tag in ('add', 'mul'):
        op = ' + ' if tag == 'add' else ' × '
        return f"({show_v2(e[1])}{op}{show_v2(e[2])})"
    if tag == 'if0':
        return f"(if0 {show_v2(e[1])} then {show_v2(e[2])} else {show_v2(e[3])})"
    if tag == 'let':
        return f"(let {e[1]} = {show_v2(e[2])} in {show_v2(e[3])})"
    raise ValueError(tag)

# ── Test: shadowing ──────────────────────────────────────────
# let x = 5 in (let x = x + 1 in (x × x))
P2 = let('x', num(5),
         let('x', add(('var', 'x'), num(1)),
             mul(('var', 'x'), ('var', 'x'))))

print("big-step:", big_step_v2(P2))       # 36 — ভেতরের x = 6

value, trace = [], []
e = P2
while not is_value(e):
    e = step_v2(e)
    trace.append(show_v2(e))              # প্রতিটা intermediate term
print("small-step:", e[1])                # 36 — একই উত্তর
for i, t in enumerate(trace):
    print(f"  step {i}: {t}")

প্রত্যাশিত output:

big-step: 36
small-step: 36
  step 0: (let x = (5 + 1) in (x × x))
  step 1: (let x = 6 in (x × x))
  step 2: (6 × 6)
  step 3: 36

তিনটা গভীর পর্যবেক্ষণ:

1. Environment (big-step) বনাম substitution (small-step) — দুইটা binding-এর দুই বাস্তবায়ন: একটা lookup-table বহন করে, অন্যটা variable-কেই মান দিয়ে replace করে দেয়। Interpreter design-এ এই দুই স্টাইল আজও coexist।
2. Shadowing-টা দুই স্টাইলে ভিন্নভাবে সমাধান — big-step-এ নতুন dict-entry পুরনোটাকে ঢেকে দেয়; small-step-এ subst-এর y == x special-case। Trace-এর step 0-এ দেখুন: বাইরের let substitute হয়েছে, কিন্তু ভেতরের let x = ...-এর body অক্ষত — নইলে উত্তর 36-এর বদলে ভুল হতো।
3. Naive substitution-এর সীমা: function (lambda) যোগ করলেই capture problem ধরা পড়বে — variable-এর নাম দুই scope-এ টক্কর খায়। Real systems α-renaming বা de Bruijn index ব্যবহার করে; compilers module-এ এটা ফিরবে।

নিজে বাড়ান:

1. Unbound variable দিয়ে চালান — let-ছাড়া bare 'var' node। Small-step কোথায় STUCK হয় trace-এ দেখুন; big-step-এ কী ঘটে (KeyError) তুলনা করুন।
2. div operator যোগ করুন যার rule শুধু divisor ≠ 0-তে apply হয় — division-by-zero-কে stuck state হিসেবে লিখুন, exception না।
3. চ্যালেঞ্জ: while-এর জন্য small-step rule লিখুন (while b do s → if b then (s; while b do s) else unit) — এবং দেখুন non-terminating program-এ big-step কখনো ফেরে না কিন্তু small-step চিরকাল step নেয়।