Foundationপ্রথম নীতি থেকে
LEVEL 13লেসন ১৬/২৩অ্যাডভান্সড১ ঘণ্টা

Type Theory ও Curry-Howard — প্রমাণ আসলে প্রোগ্রাম

Type Theory and the Curry-Howard Correspondence

Untyped lambda calculus-এ টাইপ যোগ করলে Ω-এর মতো infinite loop ব্যাকরণগতভাবেই বাতিল হয়ে যায় — আর সেই একই টাইপিং নিয়ম, অবাক করা মিল, ঠিক প্রমাণ-লেখার নিয়মও। একটা type-checker আসলে একটা proof-checker; Coq/Agda/Lean-এ এভাবেই CompCert আর seL4-এর মতো সফটওয়্যার machine-verified হয়।

এই লেসন শেষে আপনি পারবেন

  • Simply-typed lambda calculus-এর টাইপিং নিয়ম প্রয়োগ করে একটা term-এর টাইপ derive করতে পারবেন
  • কেন Ω STLC-তে টাইপ-চেক করতে ব্যর্থ হয় তা ব্যাখ্যা করে strong normalization ও Turing-completeness sacrifice-এর trade-off বলতে পারবেন
  • Curry-Howard correspondence নির্ভুলভাবে বর্ণনা করতে পারবেন — proposition as type, proof as program
  • Implication↔function type, conjunction↔product type, disjunction↔sum type — এই correspondence concrete term লিখে দেখাতে পারবেন
  • Dependently-typed proof assistant (Coq/Agda/Lean) কীভাবে CompCert ও seL4-এর মতো বাস্তব সফটওয়্যার machine-verify করে তা ব্যাখ্যা করতে পারবেন

আগে যা বোঝা থাকা দরকার

আগে এটা বুঝি

২০০৫ সালে Georges Gonthier একটা ১২৪ বছরের পুরনো গাণিতিক সমস্যা — Four Color Theorem — সম্পূর্ণভাবে Coq নামের একটা প্রোগ্রামিং টুলে formalize করেন। প্রমাণটা এত জটিল যে কোনো মানুষ হাতে পুরোপুরি যাচাই করতে পারবে না বলে ১৯৭৬ সালের মূল প্রমাণ (যা কম্পিউটার-সহায়তায় হাজার হাজার case যাচাই করেছিল) নিয়ে গণিতবিদদের মধ্যে সন্দেহ ছিল।

Gonthier-এর সমাধান অদ্ভুত শোনায়: তিনি প্রমাণটাকে একটা প্রোগ্রাম হিসেবে লিখলেন, আর Coq-এর type checker সেটা “চালিয়ে” verify করল। কোনো আলাদা “proof checker” লাগেনি — যে যন্ত্রটা একটা প্রোগ্রামের টাইপ চেক করে, সেই একই যন্ত্র একটা গাণিতিক প্রমাণও চেক করে ফেলল।

এটা কাকতালীয় সুবিধা না। এর পেছনে আছে বিংশ শতাব্দীর সবচেয়ে চমকপ্রদ গাণিতিক পর্যবেক্ষণগুলোর একটা, যেটা এই লেসনের কেন্দ্রীয় বিষয়:

একটা প্রস্তাবনার (proposition) প্রমাণ, আর একটা প্রোগ্রাম — এই দুটো জিনিস, ঠিক গাণিতিকভাবে, একই জিনিস।

এটাকে বলা হয় Curry-Howard correspondence। এটা বোঝার জন্য আমাদের আগে cs-theory/lambda-calculus-এ যা শিখেছি তার উপর একটা নতুন স্তর বসাতে হবে — type।

মূল ধারণা

Simply-Typed Lambda Calculus (STLC)

cs-theory/lambda-calculus-এ untyped lambda calculus-এ যেকোনো term ব্যাকরণগতভাবে বৈধ ছিল — এমনকি Ω = (λx. x x) (λx. x x), যা চিরকাল লুপ করে। এখন আমরা প্রতিটা term-এ একটা টাইপ যোগ করব, আর দেখব এই সামান্য শৃঙ্খলাই Ω-এর মতো term-কে ব্যাকরণগতভাবেই বাতিল করে দেয়।

টাইপ

τ ::= base type (যেমন Bool, Nat)
    | τ1 → τ2      (function type)

τ1 → τ2 মানে “যে ফাংশন τ1-টাইপের একটা input নেয় আর τ2-টাইপের output দেয়”।

Typing judgment

Γ⊢e:τ\Gamma \vdash e : \tau

পড়া হয়: “context Γ-তে (যেখানে প্রতিটা free variable-এর একটা ঘোষিত টাইপ আছে), term e-এর টাইপ τ।” Γ একটা list যেমন x:Bool, y:Nat।

টাইপিং নিয়ম — তিনটা, ঠিক lambda calculus-এর তিনটা construct-এর মতো

Var:

x:τ∈ΓΓ⊢x:τ\frac{x{:}\tau \in \Gamma}{\Gamma \vdash x : \tau}

“যদি x-এর টাইপ τ বলে context-এ ঘোষিত থাকে, তাহলে x-এর টাইপ τ।”

Abs:

Γ,x:τ1⊢e:τ2Γ⊢λx:τ1. e : τ1→τ2\frac{\Gamma, x{:}\tau_1 \vdash e : \tau_2}{\Gamma \vdash \lambda x{:}\tau_1.\, e \ :\ \tau_1 \to \tau_2}

“যদি x-এর টাইপ τ1 ধরে নিয়ে e-এর টাইপ τ2 বের করা যায়, তাহলে পুরো abstraction-এর টাইপ τ1 → τ2।” (লক্ষ্য করুন এখন প্রতিটা abstraction-এ parameter-এর টাইপ ঘোষণা করতে হয়: λx:τ1. e।)

App:

Γ⊢e1:τ1→τ2Γ⊢e2:τ1Γ⊢e1 e2 : τ2\frac{\Gamma \vdash e_1 : \tau_1 \to \tau_2 \qquad \Gamma \vdash e_2 : \tau_1}{\Gamma \vdash e_1\ e_2 \ :\ \tau_2}

“যদি e1-এর টাইপ τ1 → τ2 হয়, আর e2-এর টাইপ ঠিক τ1 (input-এর টাইপ মেলে), তাহলে প্রয়োগের ফলাফল τ2।”

একটা worked derivation

⊢λx:Nat. x : Nat→Nat\vdash \lambda x{:}\text{Nat}.\, x \ :\ \text{Nat} \to \text{Nat}

প্রমাণ: Abs rule প্রয়োগ করতে হবে x:Nat ⊢ x : Nat — যা সরাসরি Var rule (x:Nat context-এই আছে)। Abs rule তখন দেয় ⊢ λx:Nat. x : Nat → Nat। ∎

এবার একটা application:

(λx:Nat. x) 5 : Nat(\lambda x{:}\text{Nat}.\, x)\ 5 \ :\ \text{Nat}

App rule: e1 = λx:Nat.x টাইপ Nat→Nat (উপরে প্রমাণিত), e2 = 5 টাইপ Nat (সরাসরি literal), input টাইপ মেলে (Nat = Nat), তাই ফলাফল Nat। ✓

কেন Ω STLC-তে টাইপ-চেক হয় না — আর কেন এটা গুরুত্বপূর্ণ

Ω = (λx. x x) (λx. x x)-এর ভেতরের অংশটা বিবেচনা করুন: x x — x-কে নিজের উপর প্রয়োগ করা। এটা টাইপ-চেক করতে হলে:

App rule প্রয়োগ করতে x-এর টাইপ হতে হবে τ1 → τ2 কোনো τ1, τ2-র জন্য (কারণ এটা function position-এ আছে), এবং x-এর টাইপ হতে হবে τ1 (কারণ এটা argument position-এও আছে, একই x)। তাহলে:

τ1→τ2  =  τ1\tau_1 \to \tau_2 \;=\; \tau_1

এই সমীকরণের কোনো সসীম সমাধান নেই — τ1 নিজেই নিজের একটা প্রকৃত অংশ হতে পারে না, ঠিক যেমন n = n + 1-এর কোনো সসীম সংখ্যা সমাধান নেই। তাই x x STLC-তে টাইপ-চেক করতে ব্যর্থ হয়, আর যেহেতু Ω-এর ভেতরেই x x আছে, পুরো Ω ব্যাকরণগতভাবেই বাতিল — একটা well-typed STLC term কখনোই না।

মূল্য — Turing-completeness ত্যাগ করা

কিন্তু এই গ্যারান্টির একটা দাম আছে। STLC-তে general recursion লেখা যায় না (একটা function নিজেকে সরাসরি কল করতে গেলে তার নিজের টাইপের মধ্যে নিজেকে reference করতে হয়, ঠিক x x-এর মতো একই সমস্যায় পড়ে)। তাই STLC Turing-complete না — এটা যা প্রকাশ করতে পারে তার সেট প্রকৃত Turing machine-এর চেয়ে ছোট (যদিও যথেষ্ট বড়, বেশিরভাগ বাস্তব “সসীম” গণনার জন্য যথেষ্ট)।

এটাই সরাসরি ব্যাখ্যা করে কেন total functional language (Agda-র ডিফল্ট mode, Idris-এর কিছু mode, Coq-এর Gallina) সচেতনভাবে পূর্ণ Turing-completeness ত্যাগ করে: তারা শুধু সেই প্রোগ্রামগুলো গ্রহণ করে যেগুলো প্রমাণযোগ্যভাবে থামে — general recursion-এর বদলে structural recursion (শুধু ছোট subterm-এর উপর recursive call, mathematics/induction-এর structural induction-এর মতোই well-founded) বাধ্যতামূলক করে। বিনিময়ে তারা পায় একটা বিশাল সুবিধা: টাইপ-চেক পাস মানেই termination — যা পরের বিভাগে দেখব, প্রমাণ-লেখার জন্য অপরিহার্য (একটা “প্রমাণ” যেটা কখনো শেষ হয় না, প্রমাণই না)।

তুলনা করুন সাধারণ প্রোগ্রামিং ভাষার (Java, C++, Python) টাইপ সিস্টেমের সাথে — compilers/type-checking-এ যা দেখেছেন। এগুলো সচেতনভাবে general recursion/loop অনুমতি দেয় (while, unrestricted function call) — টাইপ-চেক পাস করা এখানে termination-এর কোনো গ্যারান্টি দেয় না, কারণ এই ভাষাগুলো ইচ্ছাকৃতভাবে STLC-র সীমার বাইরে, একটা fix/general-recursion primitive যোগ করে সম্পূর্ণ Turing-complete করে তোলে।

ভেতরে কী ঘটছে

Curry-Howard Correspondence — Proposition as Type, Proof as Program

এখন মূল বিষয়ে আসি। ১৯৩৪ সালে Haskell Curry এবং ১৯৬৯ সালে William Howard — স্বাধীনভাবে, দুই ভিন্ন সময়ে — একই অদ্ভুত পর্যবেক্ষণ করেন: natural deduction-এর (গাণিতিক প্রমাণের একটা প্রমিত পদ্ধতি) নিয়ম, আর simply-typed lambda calculus-এর টাইপিং নিয়ম — এই দুটো একই syntactic কাঠামো।

Curry-Howard correspondence-এর নির্ভুল বিবৃতি:

Proposition P  ⟺  Type τP\text{Proposition } P \iff \text{Type } \tau_P Proof of P  ⟺  Term of type τP\text{Proof of } P \iff \text{Term of type } \tau_P P প্রমাণযোগ্য  ⟺  τP inhabited (কোনো closed term আছে)P \text{ প্রমাণযোগ্য} \iff \tau_P \text{ inhabited (কোনো closed term আছে)}

LogicType theory
PropositionType
ProofTerm (program)
Implication P → QFunction type τP → τQ
Conjunction P ∧ QProduct type τP × τQ
Disjunction P ∨ QSum type τP + τQ
True (⊤)Unit type — ঠিক একটা inhabitant
False (⊥)Empty type — কোনো inhabitant নেই
∀x. P(x)Dependent function type (Π type)
∃x. P(x)Dependent pair type (Σ type)
Curry-Howard correspondence — logic-এর প্রতিটা connective-এর একটা টাইপ-তাত্ত্বিক দ্বৈত।

Correspondence ১ — Implication = Function Type

একটা প্রস্তাবনা P → Q-র প্রমাণ মানে কী? Natural deduction-এর সংজ্ঞা: P-এর যেকোনো প্রমাণ দেওয়া হলে, তা থেকে Q-এর একটা প্রমাণ বানানোর একটা পদ্ধতি।

এখন τP → τQ টাইপের একটা টার্ম কী? সংজ্ঞা: τP-টাইপের যেকোনো value দেওয়া হলে, τQ-টাইপের একটা value ফেরত দেওয়ার একটা ফাংশন।

এই দুটো সংজ্ঞা আক্ষরিকভাবে একই বাক্য — শুধু “প্রমাণ” শব্দটাকে “value” দিয়ে replace করা হয়েছে। এটাই পুরো correspondence-এর মূল সূত্র।

কংক্রিট উদাহরণ — implication-এর reflexivity (P → P):

λp:P. p\lambda p{:}P.\, p

এটাই প্রমাণ — “একটা P-এর প্রমাণ p দাও, আমি সেটাই ফেরত দিচ্ছি” — আর এটাই প্রোগ্রাম — identity function। দুটো একই টার্ম।

Correspondence ২ — Conjunction = Product Type

P ∧ Q-র একটা প্রমাণ মানে: P-এর একটা প্রমাণ, এবং Q-এর একটা প্রমাণ — দুটোই একসাথে। এটাই ঠিক product type τP × τQ-এর একটা value-এর সংজ্ঞা: একটা τP-value এবং একটা τQ-value-এর জোড়া।

  • ∧-introduction (দুইটা প্রমাণ থেকে conjunction বানানো) ↔ pair constructor: (p, q) : τP × τQ
  • ∧-elimination (conjunction থেকে একটা অংশ বের করা, P∧Q ⊢ P) ↔ projection: fst : τP × τQ → τP

কংক্রিট প্রমাণ — conjunction commutative (P∧Q → Q∧P):

λp:τP×τQ. (snd p, fst p)\lambda p{:}\tau_P \times \tau_Q.\, (\text{snd}\ p,\ \text{fst}\ p)

“একটা জোড়া p দাও, আমি তার দুই অংশ উল্টো ক্রমে জোড়া বানিয়ে ফেরত দিচ্ছি” — এটাই প্রমাণ, এটাই প্রোগ্রাম।

Correspondence ৩ — Disjunction = Sum Type

P ∨ Q-র একটা প্রমাণ মানে: হয় P-এর একটা প্রমাণ, অথবা Q-এর একটা প্রমাণ — কোনটা, সেই ট্যাগ-সহ। এটাই sum type τP + τQ-এর সংজ্ঞা — Inl p (P-এর একটা প্রমাণ ধারণকারী) অথবা Inr q (Q-এর একটা প্রমাণ ধারণকারী)।

∨-elimination (case analysis) ↔ pattern matching: P∨Q-থেকে R প্রমাণ করতে হলে দুই case-ই দেখাতে হয় — ঠিক যদি P তাহলে R আর যদি Q তাহলে R উভয়টাই লাগবে।

match s with ∣Inl p⇒⋯∣Inr q⇒⋯\text{match } s \text{ with } | \text{Inl}\ p \Rightarrow \cdots | \text{Inr}\ q \Rightarrow \cdots

উদাহরণ

আরেকটা সম্পূর্ণ worked example — Implication-এর transitivity

একটা সামান্য কম তুচ্ছ প্রমাণ: (P→Q) → (Q→R) → (P→R) — যদি P থেকে Q প্রমাণযোগ্য, আর Q থেকে R প্রমাণযোগ্য, তাহলে P থেকে সরাসরি R-ও প্রমাণযোগ্য।

প্রমাণ (Curry-Howard টার্ম হিসেবে):

λf:(τP→τQ). λg:(τQ→τR). λp:τP.  g (f p)\lambda f{:}(\tau_P \to \tau_Q).\ \lambda g{:}(\tau_Q \to \tau_R).\ \lambda p{:}\tau_P.\ \ g\,(f\,p)

পড়া: “আমাকে P→Q প্রমাণকারী একটা ফাংশন f দাও, Q→R প্রমাণকারী একটা ফাংশন g দাও, আর P-এর একটা প্রমাণ p দাও — আমি f-কে p-তে প্রয়োগ করে Q-এর একটা প্রমাণ বানাব, তারপর g-কে সেটার উপর প্রয়োগ করে R-এর একটা প্রমাণ বানাব।”

এটাই আক্ষরিকভাবে function composition — g ∘ f। “Implication সংক্রমণশীল (transitive)“-এর প্রমাণ, আর “দুইটা ফাংশন একের-পর-এক চালানো” প্রোগ্রাম — এই দুটো জিনিস একই টার্ম, দুইভাবে পড়া।

টাইপ derivation দিয়ে যাচাই করি (App rule বারবার প্রয়োগ করে):

f:τP→τQp:τPf p:τQg:τQ→τRg (f p):τR\frac{ \dfrac{f:\tau_P\to\tau_Q \quad p:\tau_P}{f\,p : \tau_Q} \qquad g : \tau_Q \to \tau_R }{ g\,(f\,p) : \tau_R }

তাই পুরো টার্মের টাইপ (τP→τQ) → (τQ→τR) → (τP→τR) — ঠিক যা প্রমাণ করতে চেয়েছিলাম, Abs rule তিনবার প্রয়োগ করে বাইরে বের করা।

একটা প্রমাণ পড়ার দুই উপায় — একই টার্মে
  1. যুক্তিবিদ্যার দৃষ্টিতে"P→Q আর Q→R জানা থাকলে P→R প্রমাণযোগ্য" — একটা natural deduction proof
  2. টাইপ তত্ত্বের দৃষ্টিতে"টাইপ (P→Q)→(Q→R)→(P→R)-এর একটা inhabitant আছে" — একটা টাইপ-চেক পাস করা টার্ম
  3. প্রোগ্রামারের দৃষ্টিতে"দুইটা ফাংশন কম্পোজ করলে তৃতীয়টা পাওয়া যায়" — একটা compose ফাংশন লেখা
  4. Coq/Agda/Lean-এর দৃষ্টিতেতিনটাই আক্ষরিকভাবে একই ইনপুট — একটাই টাইপ-চেকার সব তিনটা প্রশ্নের উত্তর দেয়

বাস্তব সিস্টেমে

যেখানে এই correspondence সত্যিই সফটওয়্যার বদলায়

Dependently-typed proof assistant — Coq, Agda, Lean। এই ভাষাগুলো STLC-র function/product/sum type-কে dependent করে সম্প্রসারিত করে — একটা টাইপ এখন একটা মান-এর উপর নির্ভর করতে পারে। ∀x. P(x) (dependent function type, Π) আর ∃x. P(x) (dependent pair type, Σ) দিয়ে পুরো first-order logic (শুধু propositional না) প্রকাশ করা যায়। একটা vector-এর দৈর্ঘ্য তার টাইপে এনকোড করা যায় (Vec n τ) — “দুইটা দৈর্ঘ্য m আর n-এর vector জোড়া দিলে দৈর্ঘ্য m+n-এর vector পাওয়া যায়” এমন একটা দাবি টাইপ-checker কম্পাইল-টাইমে যাচাই করে দেয়, রানটাইমে কোনো check ছাড়াই।

একটা প্রমাণ লেখা মানে একটা প্রোগ্রাম লেখা, আর সেটা চেক করা মানে টাইপ-চেক চালানো। Coq-এ একটা theorem লেখার পর, আপনি “tactic” ব্যবহার করে ধাপে ধাপে তার প্রমাণ (= একটা term) নির্মাণ করেন। শেষে Qed লিখলে Coq-এর kernel সেই টার্মের টাইপ চেক করে — যদি টাইপ মেলে (অর্থাৎ প্রমাণকৃত proposition-এর সাথে মেলে), প্রমাণ গৃহীত। এটাই পুরো trust base — একটা ছোট, ভালোভাবে-যাচাই-করা type-checker kernel বিশ্বাস করলেই যথেষ্ট (একে বলে “de Bruijn criterion”)।

CompCert — একটা প্রমাণিত-সঠিক C compiler। Xavier Leroy-র দল Coq-এ একটা সম্পূর্ণ optimizing C compiler লেখেন, আর প্রমাণ করেন (Coq-এর মধ্যেই, একটা theorem হিসেবে) compilation semantic-preserving — অর্থাৎ generated assembly source program-এর সাথে সামঞ্জস্যপূর্ণ আচরণ করে, প্রতিটা input-এ, ব্যতিক্রম ছাড়া। বিখ্যাত Csmith fuzzing study (random C প্রোগ্রাম দিয়ে GCC/Clang-এ শত শত miscompilation bug খুঁজে পেয়েছিল) CompCert-এর optimized backend-এ একটাও বাগ খুঁজে পায়নি — শুধু unverified front-end অংশে। এটা এই lesson-এর বিষয়ের সবচেয়ে জোরালো বাস্তব প্রমাণ: type-checking-ভিত্তিক প্রমাণ সত্যিই real-world bug-class নির্মূল করে।

seL4 — একটা প্রমাণিত-সঠিক microkernel। Isabelle/HOL-এ (Coq-এর কাছাকাছি একটা cousin, একই Curry-Howard নীতির উপর দাঁড়ানো) seL4-এর C implementation-এর একটা formal specification-এর সাথে সম্পূর্ণ refinement proof আছে — মানে kernel-এর প্রতিটা আচরণ তার abstract spec-এর সাথে সামঞ্জস্যপূর্ণ প্রমাণিত। এভিয়েশন, ডিফেন্স, আর অন্যান্য high-assurance embedded system-এ ব্যবহৃত হয়, যেখানে একটা kernel bug বিপর্যয়কর হতে পারে।

compilers/type-checking-এর সাথে পার্থক্য। সাধারণ ভাষার (Java, TypeScript, Rust) টাইপ checker একটা decidable, সীমিত fragment যাচাই করে — “এই expression-এর shape ঠিক আছে কি না”, যা automatically, কোনো মানুষের সাহায্য ছাড়াই decide করা যায়। কিন্তু arbitrary mathematical proposition (যেমন Four Color Theorem) প্রমাণ করতে মানুষকেই proof term (বা tactic script) লিখতে হয় — মেশিন শুধু সেটা চেক করে, নিজে থেকে আবিষ্কার করে না (যদিও automation/tactic engine অনেক সাহায্য করে)। এই স্পেকট্রাম-এর একপ্রান্তে Java-এর সাধারণ টাইপ checker, অন্যপ্রান্তে Coq-এর full dependent type checker — দুটোই একই Curry-Howard নীতির উপর দাঁড়ানো, শুধু expressiveness-এর মাত্রায় আলাদা।

যে ভুলগুলো সবাই করে

“Curry-Howard মানে যেকোনো টাইপ-চেকার এখন স্বয়ংক্রিয়ভাবে গাণিতিক উপপাদ্য 'প্রমাণ' করে ফেলতে পারে।”

না — টাইপ-চেকার শুধু verify করে একটা দেওয়া টার্ম আসলেই একটা নির্দিষ্ট টাইপের কি না। এটা আবিষ্কার করে না সেই টার্মটা কী হবে।

একটা টাইপ (proposition) “inhabited” কি না (অর্থাৎ প্রমাণযোগ্য কি না) তা সাধারণভাবে decide করা যায় না — সাধারণ dependently-typed system-এ এই প্রশ্ন undecidable (এমনকি সহজ propositional logic-এর জন্যও, provability decide করা NP-hard বা আরও কঠিন হতে পারে, তত্ত্বের ধরনের উপর নির্ভর করে)।

মানুষ (বা একটা automated tactic/proof-search engine, যা নিজেও heuristic-নির্ভর, guarantee-free) proof term-টা নির্মাণ করে; টাইপ-চেকার শুধু সেই নির্মাণ শুদ্ধ কি না তা mechanically, দ্রুত, নির্ভরযোগ্যভাবে যাচাই করে। “প্রমাণ খোঁজা” আর “প্রমাণ চেক করা” — কম্পিউটেশনাল complexity-র দৃষ্টিতে সম্পূর্ণ ভিন্ন দুইটা কাজ, ঠিক cs-theory-র NP-completeness লেসনে “সমাধান খোঁজা কঠিন, যাচাই করা সহজ” পার্থক্যের একটা প্রতিফলন।

“Dependent typing মানে শুধু বেশি annotation লেখা, মূলত সাধারণ static typing-এর মতোই।”

গুণগতভাবে ভিন্ন। সাধারণ static typing-এ (STLC, Hindley-Milner) একটা টাইপ শুধু একটা shape বর্ণনা করে — “একটা integer”, “একটা list of integer” — টাইপ কখনো একটা নির্দিষ্ট মান সম্পর্কে কিছু বলে না।

Dependent typing-এ টাইপ মান-এর উপর নির্ভর করতে পারে — Vec n τ মানে “দৈর্ঘ্য ঠিক n-এর একটা vector”, যেখানে n নিজে একটা runtime মান। এর মানে টাইপ-চেকার এখন এমন দাবি যাচাই করতে পারে যা সাধারণ টাইপ সিস্টেমে অপ্রকাশযোগ্য: “এই ফাংশন সবসময় একটা সাজানো list ফেরত দেয়”, “এই index সবসময় array-এর সীমার মধ্যে”, “এই দুইটা matrix-এর dimension গুণ করার জন্য উপযুক্ত”। এগুলো সাধারণ টাইপ সিস্টেমে হয় runtime check হিসেবে থাকে (ব্যর্থ হতে পারে) অথবা প্রোগ্রামারের মাথায় informal invariant হিসেবে থাকে (ভুলে যাওয়া যায়) — dependent typing-এ এগুলো compile-time-এ mechanically যাচাই হওয়া গ্যারান্টি।

“'Formally verified' (যেমন CompCert, seL4) মানে সেই সফটওয়্যারে কোনো bug নেই, একদম নিশ্চিতভাবে।”

cs-theory/formal-methods-hoare-logic-model-checking-tla-এ একই সতর্কতা দিয়েছিলাম, এখানেও প্রযোজ্য — বরং আরও স্পষ্টভাবে।

“Formally verified” মানে: implementation একটা নির্দিষ্ট formal specification মেনে চলে, এটা প্রমাণিত। কিন্তু নিশ্চয়তার বৃত্তটার বাইরে এখনও কয়েকটা জায়গা থেকে যায়:

  • Specification নিজে ভুল বা অসম্পূর্ণ হতে পারে — CompCert প্রমাণ করে compilation semantic-preserving, কিন্তু যদি C standard-এর formal semantics-ই কোনো real-world edge case ভুলভাবে ধরে থাকে, সেই ভুল প্রমাণের মধ্য দিয়েও বেঁচে যায়।
  • প্রমাণ-চেকার kernel নিজেই বিশ্বাসযোগ্য হতে হবে — Coq-এর ছোট trusted kernel-এ যদি কোনো bug থাকে (বিরল, কিন্তু ইতিহাসে ঘটেছে), তার উপর দাঁড়ানো সব প্রমাণের নিশ্চয়তা প্রশ্নবিদ্ধ হয়ে যায়।
  • Hardware ও compiler-below-the-model — একটা প্রমাণিত-সঠিক algorithm ভুল hardware-এ (bit flip, cosmic ray, manufacturing defect) ভুল ফলাফল দিতে পারে; সেই স্তরের নিশ্চয়তা formal verification-এর scope-এর বাইরে।

তাই সঠিক বাক্য: formal verification trusted computing base-কে নাটকীয়ভাবে সংকুচিত করে (পুরো compiler/kernel থেকে একটা ছোট proof kernel-এ), সম্পূর্ণ অদৃশ্য করে না।

বুঝেছেন কি না দেখুন

1

STLC typing rule ব্যবহার করে derive করুন: λf:(Bool→Bool). λb:Bool. f (f b)-এর টাইপ কী?

প্রয়োগ

বাইরে থেকে ভেতরে যাই।

f : Bool→Bool, b : Bool — context-এ ধরে নিয়ে ভেতরের f (f b)-এর টাইপ বের করি।

ভেতরের f b: App rule — f : Bool→Bool, b : Bool (input টাইপ মেলে) ⟹ f b : Bool।

বাইরের f (f b): App rule আবার — f : Bool→Bool, (f b) : Bool (input টাইপ মেলে, যেহেতু f b : Bool এইমাত্র প্রমাণিত) ⟹ f (f b) : Bool।

এখন Abs rule দুইবার বাইরে বের করি:

f:(Bool→Bool), b:Bool ⊢ f(f b) : Bool ⟹ (Abs, b-এর উপর) f:(Bool→Bool) ⊢ λb:Bool. f(f b) : Bool→Bool ⟹ (Abs, f-এর উপর) ⊢ λf:(Bool→Bool). λb:Bool. f(f b) : (Bool→Bool)→Bool→Bool

টাইপ: (Bool→Bool) → Bool → Bool। ব্যাখ্যা: এই ফাংশন একটা Bool→Bool ফাংশন f নেয়, তারপর একটা Bool b নেয়, আর f-কে b-এর উপর দুইবার প্রয়োগ করে ফেরত দেয় — এটাই আসলে Church numeral 2-এর typed সংস্করণ (cs-theory/lambda-calculus-এর Church numeral encoding মনে করুন — f-কে n বার প্রয়োগ করা)।

2

কেন λf:(τ→τ). λx:τ. f(f(f x)) টাইপ-চেক করে (Church numeral 3-এর typed রূপ), কিন্তু λf. λx. f (x x) STLC-তে কোনো টাইপ পায় না? দুটোর পার্থক্য ঠিক কোথায়?

যুক্তি

প্রথমটা: প্রতিটা f প্রয়োগ একই argument-টাইপে হচ্ছে — f : τ→τ, প্রতিবার input τ টাইপের কিছু নেয়, output τ টাইপের কিছু দেয়, যা পরের প্রয়োগে আবার input হিসেবে ব্যবহারযোগ্য (কারণ output-টাইপ আর input-টাইপ একই, τ)। কোনো সমস্যা নেই — শৃঙ্খলটা সঙ্গতিপূর্ণ।

দ্বিতীয়টা: x x — x-কে নিজের উপর প্রয়োগ করা হচ্ছে। App rule প্রয়োগ করতে x-এর টাইপ একই সাথে দুইটা ভূমিকায় লাগবে: function position-এ (তাই টাইপ τ1 → τ2 কোনো τ1, τ2) এবং argument position-এ (তাই টাইপ τ1)। মানে x-এর টাইপ একই সাথে τ1→τ2 এবং τ1 হতে হবে — অর্থাৎ τ1 = τ1 → τ2।

এটাই লেসনের মূল টেক্সটের সেই সমীকরণ, যার কোনো সসীম সমাধান নেই (একটা টাইপ নিজের একটা প্রকৃত উপাদান হতে পারে না STLC-র সসীম, inductively-defined টাইপ ভাষায়) — ঠিক যেমন n = n+1-এর কোনো সসীম সংখ্যা সমাধান নেই।

পার্থক্যের সারমর্ম: প্রথমটায় প্রতিটা প্রয়োগ ভিন্ন occurrence-এ হচ্ছে যদিও একই টাইপ ব্যবহার করছে — কোনো self-reference নেই। দ্বিতীয়টায় একটা একক variable একই সাথে দুই ভূমিকায় প্রয়োগ হচ্ছে, যা একটা স্ববিরোধী (self-referential) টাইপ সমীকরণ তৈরি করে। এই পার্থক্যটাই মূলত ব্যাখ্যা করে কেন Ω-এর মতো self-application-নির্ভর non-terminating term STLC-তে কখনো টাইপ পায় না — self-application মানেই একটা infinite/সসীম-অসম্ভব টাইপ সমীকরণ।

3

Curry-Howard-এর টেবিল অনুযায়ী, False (⊥) একটা Empty type-এর সাথে মেলে — এমন একটা টাইপ যার কোনো inhabitant (value) নেই। “⊥ → P যেকোনো P-এর জন্য প্রমাণযোগ্য” (ex falso quodlibet, মিথ্যা থেকে যেকোনো কিছু অনুসরণ করে) — এই যুক্তিবিদ্যার সত্যটা টাইপ তত্ত্বে কীভাবে প্রতিফলিত হয়?

যুক্তি

⊥ → P টাইপের মানে (Curry-Howard অনুযায়ী): “একটা ফাংশন যা Empty type-এর একটা value নেয়, আর τP-টাইপের একটা value ফেরত দেয়।”

এই ফাংশনটা কি লেখা সম্ভব? হ্যাঁ — vacuously (তুচ্ছভাবে)। যেহেতু Empty type-এর কোনো value-ই নেই (এটাই তার সংজ্ঞা), এই ফাংশনটাকে কখনো কোনো argument নিয়ে চালাতেই হবে না। ফাংশনটা এমন যে কোনো টাইপের জন্য লেখা যায় — টাইপ-চেকার শুধু দেখে “input যদি Empty type-এর হয়, body-টা টাইপ-সঙ্গত হতে হবে”— কিন্তু যেহেতু কখনো input আসবেই না (কোনো value নেই যা দেওয়া যায়), body-তে কোনো constraint নেই যা আসলে পরীক্ষিত হবে।

বাস্তব ভাষায় এটাকে বলে absurd function (Idris, Agda-তে আক্ষরিক নাম) — টাইপ ⊥ → P যেকোনো P-এর জন্য, একবার লেখা।

এই একই প্যাটার্ন যুক্তিবিদ্যায়: “মিথ্যা থেকে যেকোনো কিছু অনুসরণ করে” (ex falso quodlibet) ঠিক এই কারণেই সত্য — একটা মিথ্যা premise থেকে কোনো নির্দিষ্ট উপসংহারই বাদ দেওয়া যায় না, কারণ premise-টা কখনোই সত্যিকারভাবে satisfy হয় না, তাই “যদি premise সত্য হয়” শর্তটা vacuously হয়ে যায় (ঠিক এই lesson-এর আগের formal-methods লেসনে {true} while true do skip {Q} যেকোনো Q-এর জন্য partial-correct হওয়ার একই যুক্তি — vacuous truth উভয় জায়গাতেই একই কাঠামোগত কারণে কাজ করছে)।

4

Curry-Howard টার্ম লিখুন যা প্রমাণ করে (P ∧ Q) → P (conjunction-এর প্রথম অংশ বের করা যায়), আর দেখান এর টাইপ কী হবে।

প্রয়োগ

λp:τP×τQ.  fst p\lambda p{:}\tau_P \times \tau_Q.\ \ \text{fst}\ p

পড়া: “একটা জোড়া p (যা P আর Q উভয়ের প্রমাণ ধারণ করে) দাও, আমি প্রথম অংশটা বের করে ফেরত দিচ্ছি — যা P-এর একটা প্রমাণ।”

টাইপ derivation:

p : τP × τQ context-এ ধরে নিলে, fst : (τP × τQ) → τP (product type-এর প্রথম projection, একটা built-in/derived operation), তাই fst p : τP — App rule সরাসরি।

Abs rule বাইরে বের করে: ⊢ λp:(τP×τQ). fst p : (τP × τQ) → τP।

Curry-Howard-এ এটাই (P ∧ Q) → P-এর প্রমাণ — যুক্তিবিদ্যায় একে বলা হয় ∧-elimination (বাম), আর টাইপ তত্ত্বে এটা শুধু একটা projection function। দুটো নাম, একই জিনিস — ঠিক লেসনের কেন্দ্রীয় দাবি অনুযায়ী।

5

একটা প্রপোজিশন P ∨ ¬P (“হয় P, নয়তো P-এর নিষেধ” — excluded middle) বিবেচনা করুন। Curry-Howard-এর আলোকে ব্যাখ্যা করুন কেন এই প্রপোজিশনের একটা সাধারণ (P কী তা না জেনে) সরাসরি প্রমাণ-টার্ম লেখা কঠিন/অসম্ভব constructive/intuitionistic type theory-তে (যা Coq/Agda-র ভিত্তি), যদিও classical logic-এ এটা axiom হিসেবে ধরে নেওয়া হয়।

ডিজাইন

P ∨ ¬P-এর একটা প্রমাণ-টার্ম মানে (Curry-Howard অনুযায়ী) Sum type τP + (τP → ⊥)-এর একটা closed term — অর্থাৎ হয় Inl p (একটা τP-value ধারণকারী), অথবা Inr f (একটা τP → ⊥ ফাংশন ধারণকারী, মানে ¬P-এর প্রমাণ)।

সমস্যা: একটা সাধারণ (generic, P কী নির্দিষ্টভাবে না জেনে) টার্ম লিখতে হলে, প্রোগ্রামটাকে অবশ্যই decide করতে হবে কোন branch নিতে হবে (Inl না Inr) — কিন্তু arbitrary P-এর জন্য এমন কোনো mechanical, সবসময়-কাজ-করা পদ্ধতি নেই (কারণ P নিজে সিদ্ধান্তহীন/undecidable হতে পারে, যেমন cs-theory-র halting problem-সংক্রান্ত কোনো প্রপোজিশন)। Constructive logic-এ একটা প্রমাণ মানে একটা নির্মাণ পদ্ধতি — শুধু “একটা উত্তর অবশ্যই আছে” বলা যথেষ্ট না, কোনটা সেই উত্তর তা mechanically বের করতে পারতে হবে। P-এর ভেতরে যদি একটা undecidable প্রশ্ন লুকিয়ে থাকে, এই নির্মাণ সাধারণভাবে সম্ভব না।

Classical logic এর বিপরীতে excluded middle-কে axiom হিসেবে সরাসরি ধরে নেয় — “হয় P সত্য নয়তো মিথ্যা, প্রমাণ ছাড়াই, শুধু logic-এর নিয়ম হিসেবে”। এটা গাণিতিক যুক্তির জন্য প্রায়ই সুবিধাজনক (contradiction দিয়ে প্রমাণ, mathematics/proof-techniques-এ দেখা proof by contradiction ঠিক এই axiom-এর উপর নির্ভর করে), কিন্তু Curry-Howard-এর দৃষ্টিতে এটা এমন একটা “প্রমাণ” যার সাথে কোনো সরাসরি program সংশ্লিষ্ট না — এটা compute করে না, শুধু দাবি করে।

ডিজাইনের ফলাফল: Coq/Agda-এর মতো intuitionistic (constructive) type theory ডিফল্টভাবে excluded middle-কে axiom হিসেবে অন্তর্ভুক্ত করে না — যোগ করতে চাইলে explicit ভাবে axiom হিসেবে import করতে হয় (Classical module Coq-এ), আর তখন সেই অংশের প্রমাণ থেকে আর executable প্রোগ্রাম বের করা যায় না (কারণ axiom-টার সাথে কোনো টার্ম নেই, শুধু একটা ধরে-নেওয়া সত্য)। এই সিদ্ধান্তটা সরাসরি এই lesson-এর কেন্দ্রীয় নীতি থেকে আসে: যদি আপনি চান প্রতিটা প্রমাণ একটা চলমান প্রোগ্রাম হোক, আপনাকে এমন logic ব্যবহার করতে হবে যেখানে প্রতিটা প্রমাণ-নিয়মের পেছনে একটা কার্যকর নির্মাণ-পদ্ধতি আছে — আর excluded middle, সাধারণভাবে, সেই শর্ত ভাঙে।

এরপর কী

আমরা দেখলাম computation-কে দুইভাবে বোঝা যায়: রাষ্ট্র বদলানোর একটা প্রক্রিয়া হিসেবে (Hoare logic, model checking), অথবা বিশুদ্ধ function-composition হিসেবে (lambda calculus, এখন type theory-সহ)। দুইটাই এই module-এর “computation কী, আর তার সীমা কোথায়” প্রশ্নের অংশ।

পরের লেসনে আমরা সম্পূর্ণ ভিন্ন একটা প্রশ্নে যাব — computation কী করতে পারে তা না, বরং তথ্য নিজে কী, আর কতটুকু তথ্য একটা বার্তায় আসলে আছে। Shannon-এর entropy দিয়ে আমরা মাপব একটা এলোমেলো উৎস গড়ে কত bit “বহন করে” — একটা প্রশ্ন যা সরাসরি compression, নেটওয়ার্কের error-correcting code, আর এই module-এরই পরের একটা লেসনে (AI/ML foundations) ফিরে আসবে cross-entropy loss হিসেবে।

আরও পড়ুন

  • Types and Programming Languages, Chapters 9–11 — Benjamin C. Pierce · Simply-typed lambda calculus আর typing rule-এর canonical, rigorous পাঠ
  • Propositions as Types — Philip Wadler · Communications of the ACM, 2015 — Curry-Howard-এর ইতিহাস ও তাৎপর্যের সবচেয়ে পঠনীয় introduction
  • Formal Verification of a Realistic Compiler (CompCert) — Xavier Leroy · Communications of the ACM, 2009 — Coq-এ প্রমাণিত একটা প্রোডাকশন-গ্রেড C compiler-এর কেস স্টাডি