Operational Semantics
অপারেশনাল সিমান্টিক্স
ভাষার অর্থ বোঝানোর উপায় — abstract machine-এর transition rule; 'এই configuration এই step-এ ওটা হয়' শৈলী।
also: small-step semantics, big-step semantics
Small-step (structural operational semantics):
⟨x := 5; S, σ⟩ → ⟨S, σ[x↦5⟩]⟩ (assignment এক step)
if b then S else T, σ → S, σ (b true হলে)- Small-step: প্রতি reduction এক ধাপ — non-termination সহজে দেখায়, concurrency modeling-এ শক্তিশালী
- Big-step: expression → value এক judgment-এ — interpreter লেখার spec হিসেবে সরাসরি ব্যবহারযোগ্য
- Type safety proof-এর অন্য পা: progress (well-typed term step নেয় বা value) + preservation (step-এর পরেও well-typed)
- Interpreter = operational semantics-এর executable রূপ — এই কারণে teaching language-গুলো spec হিসেবে ML-এ লেখা হয়