Proof Techniques — 'কাজ করে' থেকে 'কাজ করতে বাধ্য'
Proof Techniques
Direct, contrapositive, contradiction, cases, counterexample — পাঁচটা হাতিয়ার যা দিয়ে একটা দাবি সব ক্ষেত্রে সত্য প্রমাণ করা যায়, শুধু যেসব ক্ষেত্রে টেস্ট করেছেন সেগুলোতে নয়।
আগে এটা বুঝি
আপনার একটা function আছে। আপনি ১০,০০০টা test চালালেন। সব পাশ।
Function-টা কি ঠিক?
উত্তর: জানি না।
int32 -এর একটা parameter-এর সম্ভাব্য মান ৪২৯ কোটির বেশি। দুইটা
parameter হলে সংখ্যাটা ১.৮ × ১০¹⁹। ১০,০০০টা test মানে সেই সমুদ্রের
এক ফোঁটা।
Testing একটা existential হাতিয়ার — এটা ∃input (bug) প্রমাণ করতে পারে।
কিন্তু আপনার দরকার একটা universal গ্যারান্টি: ∀input (correct)।
গত লেসনে আমরা দেখেছি এই দুইটার প্রমাণভার সম্পূর্ণ আলাদা। ∀ প্রমাণ
করতে হলে example যথেষ্ট নয় — argument লাগে।
সেই argument লেখার নিয়মতান্ত্রিক পদ্ধতিগুলোই এই লেসনের বিষয়।
মূল ধারণা
প্রমাণ আসলে কী
একটা proof হলো যুক্তির একটা শৃঙ্খল যা ইতিমধ্যে গৃহীত সত্য থেকে শুরু করে, প্রতিটা ধাপে বৈধ inference rule প্রয়োগ করে, লক্ষ্য দাবিতে পৌঁছায়।
তিনটা উপাদান:
- Axiom / গৃহীত সত্য — যা প্রমাণ ছাড়াই মেনে নিচ্ছি
- Inference rule — এক সত্য থেকে আরেক সত্যে যাওয়ার বৈধ পদক্ষেপ
- Conclusion — যা প্রমাণ করতে চাই
সবচেয়ে মৌলিক inference rule হলো modus ponens:
p → q সত্য
p সত্য
────────────
∴ q সত্যআর তার যমজ modus tollens:
p → q সত্য
¬q সত্য
────────────
∴ ¬p সত্যদ্বিতীয়টা আসলে contrapositive-এর প্রয়োগ, আর এটাই বৈজ্ঞানিক পদ্ধতির ভিত্তি: তত্ত্ব যদি X ভবিষ্যদ্বাণী করে, আর X ঘটে না, তাহলে তত্ত্ব ভুল।
হাতিয়ার ১: Direct proof
দাবি p → q প্রমাণ করতে: ধরে নিন p সত্য, যুক্তি দিয়ে q-তে পৌঁছান।
সবচেয়ে সরল, আর প্রথমে সবসময় এটাই চেষ্টা করা উচিত।
দাবি:
nজোড় হলেn²জোড়।
প্রমাণ. ধরি n জোড়। জোড়ের সংজ্ঞা অনুযায়ী কোনো পূর্ণসংখ্যা k আছে
যেন n = 2k।
তাহলে:
যেহেতু 2k² একটা পূর্ণসংখ্যা, n² কে 2 × (পূর্ণসংখ্যা) আকারে লেখা গেল।
সংজ্ঞা অনুযায়ী n² জোড়। ∎
লক্ষ্য করুন গঠনটা:
- অনুমান স্পষ্ট করে বলা
- সংজ্ঞা প্রয়োগ করে অনুমানকে সমীকরণে রূপ দেওয়া
- বীজগণিত
- লক্ষ্য-সংজ্ঞার আকারে ফিরে আসা
হাতিয়ার ২: Contrapositive
p → q প্রমাণ করা কঠিন হলে, সমতুল্য ¬q → ¬p প্রমাণ করুন।
গত লেসনে দেখেছি এরা logically equivalent। তাই একটা প্রমাণ করলেই হলো।
দাবি:
n²জোড় হলেnজোড়।
Direct চেষ্টা করলে: “ধরি n² = 2k… তাহলে n = √(2k)…” — আটকে গেলাম।
বর্গমূল নিয়ে পূর্ণসংখ্যার যুক্তি করা কঠিন।
Contrapositive: n বিজোড় হলে n² বিজোড়।
প্রমাণ. ধরি n বিজোড়, অর্থাৎ n = 2k + 1 কোনো পূর্ণসংখ্যা k-এর জন্য।
2k² + 2k পূর্ণসংখ্যা, তাই n² কে 2 × (পূর্ণসংখ্যা) + 1 আকারে
লেখা গেল — অর্থাৎ বিজোড়।
Contrapositive প্রমাণিত, তাই মূল দাবিও প্রমাণিত। ∎
হাতিয়ার ৩: Proof by contradiction
দাবি P প্রমাণ করতে: ধরে নিন ¬P, দেখান যে এতে একটা অসম্ভব ফলাফল আসে।
যেহেতু মিথ্যা কিছু থেকে অসম্ভব আসতে পারে না — আর ¬P থেকে অসম্ভব এল —
তাই ¬P মিথ্যা, অর্থাৎ P সত্য।
গণিতের সবচেয়ে বিখ্যাত প্রমাণগুলোর অনেকগুলোই এই ধরনের।
দাবি:
√2মূলদ (rational) নয়।
প্রমাণ. ধরি বিপরীতটা — √2 মূলদ। তাহলে একে a/b আকারে লেখা যায়,
যেখানে a, b পূর্ণসংখ্যা, b ≠ 0, এবং ভগ্নাংশটা সরলতম রূপে
(অর্থাৎ a আর b-এর কোনো সাধারণ উৎপাদক নেই)।
তাহলে a² জোড়। আগের দাবি অনুযায়ী (n² জোড় → n জোড়), a জোড়।
a জোড় মানে a = 2c কোনো c-এর জন্য। বসাই:
তাহলে b² জোড়, অতএব b-ও জোড়।
কিন্তু আমরা ধরেছিলাম a আর b-এর কোনো সাধারণ উৎপাদক নেই — অথচ দুটোই
জোড়, অর্থাৎ দুটোরই উৎপাদক ২। বিরোধ।
অতএব আমাদের অনুমান ভুল ছিল। √2 অমূলদ। ∎
হাতিয়ার ৪: Proof by cases
Domain-কে কয়েকটা exhaustive ক্ষেত্রে ভাগ করুন, প্রতিটার জন্য আলাদা প্রমাণ দিন।
দুইটা শর্ত মানতেই হবে:
- Exhaustive — সব সম্ভাবনা ঢাকা পড়েছে
- প্রতিটা case-এ দাবিটা সত্য
দাবি: যেকোনো পূর্ণসংখ্যা
n-এর জন্যn² + nজোড়।
প্রমাণ. দুইটা case:
Case 1: n জোড়। তাহলে n = 2k।
n² + n = n(n + 1) = 2k(2k+1) — একটা উৎপাদক 2k, তাই জোড় ✓
Case 2: n বিজোড়। তাহলে n + 1 জোড়, অর্থাৎ n + 1 = 2m।
n² + n = n(n+1) = n · 2m — জোড় ✓
প্রতিটা পূর্ণসংখ্যা হয় জোড় নয় বিজোড় (exhaustive), আর দুই ক্ষেত্রেই দাবি সত্য। ∎
আসলে এখানে আরো সরল একটা যুক্তি আছে: n² + n = n(n+1), আর পরপর দুইটা
পূর্ণসংখ্যার একটা অবশ্যই জোড়, তাই গুণফল জোড়। কিন্তু case analysis-টা
দেখিয়ে দিল পদ্ধতিটা কেমন।
হাতিয়ার ৫: Counterexample
একটা ∀ দাবি খণ্ডন করতে একটাই counterexample যথেষ্ট।
দাবি: সব মৌলিক সংখ্যা বিজোড়।
খণ্ডন. 2 মৌলিক এবং জোড়। ∎
একটা উদাহরণ, প্রমাণ শেষ।
আরেকটা, যেটা programmer-দের জন্য বেশি প্রাসঙ্গিক:
দাবি: সব
n-এর জন্যn² + n + 41মৌলিক।
n = 0 → 41 ✓ মৌলিক
n = 1 → 43 ✓
n = 2 → 47 ✓
… n = 39 পর্যন্ত সব মৌলিক!
৪০টা test case পাশ। কিন্তু:
n = 40 → 1600 + 40 + 41 = 1681 = 41² — যৌগিক।
ভেতরে কী ঘটছে
কোন হাতিয়ার কখন — একটা সিদ্ধান্ত-গাছ
- দাবিটা কী আকারের?প্রথমে গঠন চিনুন
- ∃x P(x) — একটা উদাহরণ দিনconstructive proof
- ¬∀x P(x) — একটা counterexample দিনসবচেয়ে সহজ
- p → q — direct চেষ্টা করুনp ধরে q-তে যান
- আটকে গেলে → contrapositive¬q ধরে ¬p-তে যান
- তাতেও আটকালে → contradictionp ∧ ¬q ধরে অসম্ভবে যান
- ∀n ∈ ℕ — inductionপরের লেসন
- ক্ষেত্রভেদে আচরণ আলাদা → casesexhaustive হতে হবে
Existence proof-এর দুই রকম
∃x P(x) প্রমাণের দুইটা সম্পূর্ণ আলাদা পথ আছে, আর পার্থক্যটা
computer science-এ গভীরভাবে গুরুত্বপূর্ণ।
Constructive — জিনিসটা দেখিয়ে দিন
দাবি: এমন দুইটা অমূলদ সংখ্যা
a,bআছে যেনa^bমূলদ।
এই প্রমাণটা কুখ্যাত। ধরি a = b = √2, আর দেখি √2^√2 কী।
Case 1: যদি √2^√2 মূলদ হয় — কাজ শেষ, a = b = √2 ✓
Case 2: যদি অমূলদ হয় — তাহলে নিন a = √2^√2 (অমূলদ) আর b = √2:
মূলদ ✓ ∎
কিন্তু লক্ষ্য করুন: প্রমাণটা শেষ, অথচ আমরা জানি না কোন case সত্য!
আমরা জানি এমন a, b আছে, কিন্তু বলতে পারছি না কোনটা।
একে বলে non-constructive proof।
কেন এই পার্থক্যটা CS-এ গুরুত্বপূর্ণ
একটা non-constructive proof বলে “সমাধান আছে” কিন্তু algorithm দেয় না। Computer science-এ আমাদের প্রায় সবসময় constructive প্রমাণ দরকার, কারণ প্রমাণটাই algorithm।
এই ধারণাটাই Curry–Howard correspondence-এর হৃদয়:
| Logic | Programming |
|---|---|
| Proposition | Type |
| Proof | Program |
p → q | function p -> q |
p ∧ q | tuple (p, q) |
∃x P(x) | dependent pair — মান এবং সাক্ষ্য |
Coq বা Agda-তে একটা ∃ প্রমাণ লিখলে সেই প্রমাণ থেকে আক্ষরিকভাবে
executable কোড বের করা যায়। প্রমাণটাই program।
Level 13-এ আমরা এই সংযোগটা পুরো খুলব।
একটা algorithm-এর correctness প্রমাণ
এবার এই সব হাতিয়ার একসাথে ব্যবহার করি।
def gcd(a, b):
while b != 0:
a, b = b, a % b
return aদাবি: এই function gcd(a, b) ফেরত দেয়, যেখানে a > 0, b ≥ 0।
দুইটা জিনিস প্রমাণ করতে হবে: termination আর correctness।
Termination
প্রতি iteration-এ b -এর নতুন মান a mod b, আর সংজ্ঞা অনুযায়ী
0 ≤ a mod b \< b।
তাই b -এর মান কঠোরভাবে কমছে এবং সবসময় অ-ঋণাত্মক।
অ-ঋণাত্মক পূর্ণসংখ্যার একটা কঠোরভাবে হ্রাসমান ক্রম অসীম হতে পারে না (well-ordering principle)। অতএব loop শেষ হবে। ∎
Correctness
মূল lemma:
Lemma:
b > 0হলেgcd(a, b) = gcd(b, a mod b)
প্রমাণ. ধরি r = a mod b, অর্থাৎ a = qb + r কোনো q-এর জন্য।
দেখাব দুইটা set অভিন্ন: {a, b}-এর সাধারণ ভাজক আর {b, r}-এর সাধারণ ভাজক।
(⊆) ধরি d, a আর b দুটোকেই ভাগ করে। তাহলে d | (a − qb), অর্থাৎ
d | r। সুতরাং d, b আর r দুটোকেই ভাগ করে।
(⊇) ধরি d, b আর r দুটোকেই ভাগ করে। তাহলে d | (qb + r), অর্থাৎ
d | a। সুতরাং d, a আর b দুটোকেই ভাগ করে।
দুইটা set সমান, তাই তাদের সর্বোচ্চ উপাদানও সমান:
gcd(a, b) = gcd(b, r) ∎
এখন loop invariant:
INV : gcd(a₀, b₀) = gcd(a, b)যেখানে a₀, b₀ মূল input।
- Initialization: শুরুতে
a = a₀, b = b₀, তাই স্পষ্টত সত্য ✓ - Maintenance: Lemma অনুযায়ী
gcd(a, b) = gcd(b, a mod b)— ঠিক যা iteration করছে ✓ - Termination: Loop শেষ হয়
b = 0-তে। আরgcd(a, 0) = a(কারণaনিজেকে ভাগ করে এবং সব সংখ্যা0কে ভাগ করে)। তাই return value= gcd(a, 0) = gcd(a₀, b₀)✓ ∎
এই প্রমাণটা যা দিল: এখন আমরা জানি Euclid’s algorithm সব বৈধ input-এ কাজ করে — শুধু যেগুলো test করেছি সেগুলোতে নয়। ২৩০০ বছরের পুরনো algorithm, আর প্রমাণটাও প্রায় ততটাই পুরনো।
উদাহরণ
একটা ভুল প্রমাণ ধরুন
প্রমাণ পড়ার দক্ষতা প্রমাণ লেখার মতোই গুরুত্বপূর্ণ। এই “প্রমাণ”-টা দেখুন:
দাবি:
1 = 2“প্রমাণ.” ধরি
a = b।
a = b(দেওয়া)a² = ab(দুই পাশেaগুণ)a² − b² = ab − b²(দুই পাশ থেকেb²বিয়োগ)(a+b)(a−b) = b(a−b)(উৎপাদক)a + b = b(দুই পাশকে(a−b)দিয়ে ভাগ)b + b = b(a = bবসিয়ে)2b = b2 = 1(bদিয়ে ভাগ) ∎
ভুলটা কোথায়?
ধাপ ৫। আমরা (a − b) দিয়ে ভাগ করেছি। কিন্তু a = b, তাই
a − b = 0 — শূন্য দিয়ে ভাগ।
আরো একটা সূক্ষ্ম সমস্যা ধাপ ৮-এ: b দিয়ে ভাগ করা হয়েছে, কিন্তু b = 0
হলে সেটাও অবৈধ।
Pigeonhole principle — সরলতম শক্তিশালী হাতিয়ার
nটা কবুতরmটা খোপে রাখলে, যদিn > mহয়, তবে অন্তত একটা খোপে একাধিক কবুতর থাকবে।
এতটাই স্পষ্ট যে প্রমাণ লাগে না মনে হয়। কিন্তু এর প্রয়োগ বিস্ময়কর।
প্রয়োগ ১: Hash collision অনিবার্য
দাবি: যেকোনো hash function যা যেকোনো দৈর্ঘ্যের string কে ৩২-bit মানে map করে, তার collision থাকবেই।
প্রমাণ. সম্ভাব্য input অসীম (যেকোনো দৈর্ঘ্যের string)।
সম্ভাব্য output 2³² টা — সসীম।
Pigeonhole অনুযায়ী অন্তত দুইটা (আসলে অসীম সংখ্যক) input একই output-এ map হবে। ∎
এই কারণেই কোনো hash table implementation collision handling ছাড়া লেখা যায় না। এটা “ভালো hash function বেছে নিলে এড়ানো যাবে” এমন কিছু নয় — এটা গাণিতিকভাবে অসম্ভব।
Level 6-এ আমরা collision resolution-এর কৌশলগুলো দেখব।
প্রয়োগ ২: Lossless compression সব ফাইল ছোট করতে পারে না
দাবি: এমন কোনো lossless compression algorithm নেই যা প্রতিটা ফাইলকে ছোট করে।
প্রমাণ. ধরি বিপরীতটা — এমন একটা algorithm C আছে।
n bit-এর ফাইল আছে 2ⁿ টা। C প্রতিটাকে n bit-এর কম করে, অর্থাৎ
সবগুলো output-এর দৈর্ঘ্য 0 থেকে n−1 bit।
n bit-এর কম দৈর্ঘ্যের মোট string আছে:
2ⁿ টা input কে 2ⁿ − 1 টা output-এ map করতে হচ্ছে। Pigeonhole
অনুযায়ী অন্তত দুইটা ভিন্ন input একই output দেবে।
কিন্তু তাহলে decompression অসম্ভব — কোন input থেকে এসেছে বলা যাবে না। Lossless-এর সংজ্ঞার বিরোধ। ∎
এই কারণেই ZIP ফাইল আবার ZIP করলে সাধারণত বড় হয়। Compression কাজ করে কারণ বাস্তব ডেটায় pattern থাকে — সব সম্ভাব্য bit sequence সমান সম্ভাব্য নয়। Random ডেটা compress হয় না।
Level 13-এ information theory-তে আমরা এটা Shannon entropy দিয়ে পরিমাণগতভাবে দেখব।
নিজে চালিয়ে দেখুন
Test যা মিথ্যা আত্মবিশ্বাস দেয়
def is_prime_buggy(n):
"""Euler's polynomial দিয়ে 'অপ্টিমাইজড' primality — কল্পিত bug"""
if n \< 2:
return False
for i in range(2, int(n ** 0.5) + 1):
if n % i == 0:
return False
return True
def euler_prime(n):
"""দাবি: সব n ≥ 0 -এর জন্য n² + n + 41 মৌলিক"""
return n*n + n + 41
# ── "test suite" ──
failures = 0
for n in range(40):
if not is_prime_buggy(euler_prime(n)):
print(f"✗ n={n}: {euler_prime(n)} মৌলিক নয়")
failures += 1
print(f"৪০টা test চালানো হলো, ব্যর্থ: {failures}")
print("দাবিটা কি প্রমাণিত?\n")
# ── আরেকটু চালাই ──
for n in range(40, 45):
v = euler_prime(n)
print(f"n={n:3d} → {v:6d} মৌলিক? {is_prime_buggy(v)}")Output:
৪০টা test চালানো হলো, ব্যর্থ: 0
দাবিটা কি প্রমাণিত?
n= 40 → 1681 মৌলিক? False
n= 41 → 1763 মৌলিক? False
n= 42 → 1847 মৌলিক? True
n= 43 → 1933 মৌলিক? True
n= 44 → 2021 মৌলিক? False৪০টা পরপর pass, তারপর fail। আর n = 40-এর ব্যর্থতাটা “দুর্ভাগ্যজনক”
নয় — অনিবার্য:
Property-based testing দিয়ে দ্রুত ধরা:
pip install hypothesisfrom hypothesis import given, strategies as st
@given(st.integers(min_value=0, max_value=1000))
def test_euler_always_prime(n):
assert is_prime_buggy(euler_prime(n)), f"n={n} ভাঙল"
test_euler_always_prime()Hypothesis দ্রুত n = 40 (বা 41) খুঁজে বের করবে, এবং সবচেয়ে ছোট
counterexample-এ shrink করে দেখাবে।
তবু এটা proof নয় — শুধু অনেক বেশি চতুর search। Hypothesis যদি counterexample না পেত, তার মানে হতো না যে দাবিটা সত্য।
একটা function হাজারো test পাশ করেও ভুল হতে পারে। Property-based testing অনেক বেশি input ঢাকে, কিন্তু তাও proof নয় — শুধু আরো ভালো search।
Floating point associativity — একটা counterexample খোঁজা
import random
def find_counterexample(trials=100000):
"""(a+b)+c ≠ a+(b+c) এমন float খুঁজুন"""
for _ in range(trials):
a = random.uniform(-1e10, 1e10)
b = random.uniform(-1e10, 1e10)
c = random.uniform(-1e-5, 1e-5)
if (a + b) + c != a + (b + c):
return a, b, c
return None
hit = find_counterexample()
if hit:
a, b, c = hit
print(f"a = {a!r}")
print(f"b = {b!r}")
print(f"c = {c!r}")
print(f"(a+b)+c = {(a+b)+c!r}")
print(f"a+(b+c) = {a+(b+c)!r}")
print(f"পার্থক্য = {abs(((a+b)+c) - (a+(b+c)))!r}")সহজে পাওয়া যায় — সাধারণত প্রথম কয়েকটা চেষ্টাতেই।
সবচেয়ে পরিষ্কার উদাহরণটা হাতে বানানো যায়:
>>> (1e16 + 1) - 1e16
0.0
>>> 1e16 + (1 - 1e16)
0.0
>>> (1e16 + 1.0) - 1e16 # 1 হারিয়ে গেল
0.0
>>> 1.0 + (1e16 - 1e16) # এখানে টিকে গেল
1.01e16-এর পাশে 1 যোগ করলে সেটা হারিয়ে যায়, কারণ double-এ প্রায় ১৫-১৬
দশমিক অঙ্কের নির্ভুলতা। ক্রম বদলালে ফল বদলায়।
কেন এটা গুরুত্বপূর্ণ:
-
Compiler optimization:
-ffast-mathদিলে GCC ধরে নেয় float associative, আর expression পুনর্বিন্যাস করে। ফলাফল বদলে যেতে পারে। Scientific computing-এ এটা বিপজ্জনক। -
Parallel reduction: একটা array-র যোগফল যদি ৮টা thread ভাগ করে বের করে, ক্রম আলাদা হবে, ফলাফলও সামান্য আলাদা হবে। তাই একই program একই input-এ দুইবার চালালে ভিন্ন উত্তর — reproducibility নষ্ট।
-
আর্থিক হিসাব: এই কারণেই টাকা কখনো float-এ রাখা হয় না; integer (পয়সা) বা decimal type ব্যবহার করা হয়।
Level 1-এ আমরা IEEE 754-এর ভেতরে ঢুকে দেখব ঠিক কোন bit-এ এই ত্রুটি জন্মায়।
গণিতের নিয়ম যন্ত্রে সবসময় খাটে না। (a+b)+c = a+(b+c) বাস্তব সংখ্যায় সত্য, float-এ মিথ্যা — আর এটা compiler optimization ও parallel reduction-এ সরাসরি প্রভাব ফেলে।
নিজে বানান
Runtime Contract Checker
- precondition, postcondition আর invariant-এর জন্য decorator লিখুন
- লঙ্ঘন হলে স্পষ্ট বার্তা সহ ব্যর্থ হোন
- gcd, binary search আর sorting-এ প্রয়োগ করুন
- ইচ্ছে করে bug ঢুকিয়ে দেখুন কোন contract আগে ভাঙে
প্রমাণ লেখা আর কোড লেখার মধ্যে একটা ব্যবহারিক সেতু হলো contract — কোডে লেখা assertion যা প্রমাণের অনুমানগুলো runtime-এ যাচাই করে।
import functools
class ContractError(AssertionError):
pass
def contract(pre=None, post=None):
"""
pre : (*args) -> bool — function চালানোর আগে সত্য হতে হবে
post : (result, *args) -> bool — চালানোর পর সত্য হতে হবে
"""
def decorate(fn):
@functools.wraps(fn)
def wrapper(*args, **kwargs):
if pre and not pre(*args, **kwargs):
raise ContractError(
f"{fn.__name__}: PRECONDITION ভেঙেছে args={args}")
result = fn(*args, **kwargs)
if post and not post(result, *args, **kwargs):
raise ContractError(
f"{fn.__name__}: POSTCONDITION ভেঙেছে "
f"args={args} result={result!r}")
return result
return wrapper
return decorate
# ── Euclid's algorithm, contract সহ ─────────────────────────────
def divides(d, n):
return n % d == 0
@contract(
pre = lambda a, b: a > 0 and b >= 0,
post = lambda r, a, b: (
r > 0 # ধনাত্মক
and divides(r, a) and divides(r, b) # সাধারণ ভাজক
and all(not (divides(d, a) and divides(d, b)) # সর্বোচ্চ
for d in range(r + 1, min(a, b or a) + 1))
),
)
def gcd(a, b):
while b != 0:
a, b = b, a % b
return a
print(gcd(48, 18)) # 6
print(gcd(17, 5)) # 1
print(gcd(100, 0)) # 100
try:
gcd(-4, 8)
except ContractError as e:
print("ধরা পড়ল:", e)
# ── Sorting, contract সহ ────────────────────────────────────────
from collections import Counter
@contract(
post = lambda r, arr: (
all(r[i] <= r[i+1] for i in range(len(r)-1)) # sorted
and Counter(r) == Counter(arr) # permutation
),
)
def my_sort(arr):
return sorted(arr)
@contract(
post = lambda r, arr: (
all(r[i] <= r[i+1] for i in range(len(r)-1))
and Counter(r) == Counter(arr)
),
)
def buggy_sort(arr):
"""duplicate ফেলে দেয় — sorted কিন্তু permutation নয়"""
return sorted(set(arr))
print(my_sort([3, 1, 2]))
try:
buggy_sort([3, 1, 2, 1])
except ContractError as e:
print("ধরা পড়ল:", e)লক্ষ্য করুন sorting-এর postcondition-এ দুইটা শর্ত। শুধু “sorted”
যথেষ্ট নয় — return [] তো সবসময় sorted! Permutation শর্তটাই আসল
কাজটা করে।
এটাই formal specification লেখার সবচেয়ে গুরুত্বপূর্ণ শিক্ষা: আপনার specification যদি একটা trivial ভুল implementation মেনে নেয়, তাহলে specification-টাই অসম্পূর্ণ।
নিজে বাড়ান:
invariantdecorator যোগ করুন যা প্রতিটা method call-এর আগে-পরে class-এর invariant যাচাই করে- Binary search-এর সম্পূর্ণ contract লিখুন (গত লেসনের invariant ব্যবহার করে)
- Production-এ contract বন্ধ করার ব্যবস্থা রাখুন (
python -O) - একটা stack class লিখুন এই invariant সহ:
len(items) == size, এবংpushকরেpopকরলে আগের অবস্থা ফিরে আসে hypothesisদিয়ে contract-গুলো property-based test করুন
বাস্তব সিস্টেমে
প্রমাণ শিল্পক্ষেত্রে
seL4 — verified microkernel. প্রায় ১০,০০০ লাইন C, সম্পূর্ণ formally verified। প্রমাণটা প্রায় ২,০০,০০০ লাইন Isabelle/HOL — কোডের ২০ গুণ। গ্যারান্টি: kernel কখনো crash করবে না, কখনো undefined behaviour দেখাবে না, আর binary টা specification-এর সাথে সঙ্গতিপূর্ণ। ব্যবহার হয় সামরিক ড্রোন আর চিকিৎসা যন্ত্রে।
CompCert — verified C compiler. প্রমাণিত যে compiled code সবসময় source-এর semantics রক্ষা করে। ২০১১-র একটা গবেষণায় (Csmith) দেখা গেছে GCC আর LLVM-এ শত শত miscompilation bug পাওয়া গেছে, কিন্তু CompCert-এর verified অংশে একটাও না।
AWS। S3, DynamoDB, EBS, আর তাদের নেটওয়ার্ক protocol TLA+ দিয়ে specify ও model-check করা। প্রকাশিত রিপোর্ট অনুযায়ী তারা এমন bug ধরেছে যেগুলো ৩৫ ধাপের নির্দিষ্ট ঘটনাক্রমে ঘটত — testing-এ কখনো ধরা পড়ত না। IAM policy-র জন্য তাদের Zelkova tool SMT solver দিয়ে প্রশ্নের উত্তর দেয়: “এই policy কি কোনো অবস্থায় public access দিতে পারে?”
Rust-এর borrow checker. এটা আক্ষরিকভাবে একটা proof system। Compiler প্রমাণ করে যে আপনার program-এ data race নেই এবং use-after-free নেই। প্রমাণ করতে না পারলে compile হয় না। “Fighting the borrow checker” মানে আসলে “আমার প্রমাণটা লিখতে পারছি না”।
Cryptography. প্রতিটা cryptographic protocol-এর নিরাপত্তা একটা reduction proof: “এই scheme ভাঙা গেলে discrete log সমস্যা সমাধান করা যাবে।” TLS 1.3-এর নকশা প্রক্রিয়ায় formal verification কেন্দ্রীয় ভূমিকা রেখেছে — আগের সংস্করণগুলোর যে দুর্বলতাগুলো (BEAST, CRIME, Logjam) বাস্তবে আবিষ্কৃত হয়েছিল, সেগুলো প্রমাণ থাকলে ধরা পড়ত।
Smart contract। ২০১৬-র DAO hack-এ ৫ কোটি ডলার হারানোর পর blockchain জগতে formal verification মূলধারায় এসেছে। এখন বড় protocol-গুলো Certora, K framework দিয়ে verify করা হয়।
যে ভুলগুলো সবাই করে
“Proof by contradiction আর contrapositive একই জিনিস।”
সম্পর্কিত, কিন্তু আলাদা।
Contrapositive: p → q প্রমাণ করতে ¬q → ¬p প্রমাণ করুন।
আপনি ¬q ধরে শুরু করেন এবং ¬p-তে পৌঁছান। কোনো বিরোধ লাগে না।
Contradiction: p → q প্রমাণ করতে p ∧ ¬q ধরুন এবং যেকোনো
অসম্ভব ফলাফলে পৌঁছান — সেটা ¬p হতে পারে, বা 1 = 2 হতে পারে,
বা সম্পূর্ণ অসম্পর্কিত কিছু।
Contrapositive বেশি নির্দিষ্ট, আর সাধারণত বেশি পরিষ্কার। তাই যেখানে contrapositive দিয়ে হয়, সেখানে contradiction ব্যবহার না করাই ভালো।
Constructive mathematics-এ পার্থক্যটা মৌলিক: contrapositive সবসময়
বৈধ, কিন্তু contradiction (বিশেষত ¬¬p → p রূপে) বৈধ নয়। Coq বা Agda-তে
কাজ করলে এই পার্থক্যটা প্রতিদিন সামনে আসে।
“আমার প্রমাণ আছে, তাই কোড bug-free।”
তিনটা ফাঁক থাকে।
১. Specification ভুল হতে পারে। আপনি প্রমাণ করেছেন code specification মানে। কিন্তু specification-টাই যদি ভুল চায়? seL4-ও প্রমাণ করে না যে kernel “উপযোগী” — শুধু প্রমাণ করে যে সেটা spec মানে।
২. অনুমানগুলো ভুল হতে পারে। প্রায় প্রতিটা proof কিছু ধরে নেয়: hardware ঠিকমতো কাজ করে, compiler correct, cosmic ray bit flip করে না। Rowhammer আর Spectre দেখিয়েছে এই অনুমানগুলো ভাঙতে পারে।
৩. প্রমাণে ভুল থাকতে পারে। মানুষের লেখা প্রমাণে ভুল হয় — গণিতের ইতিহাসে বহু “প্রমাণিত” theorem পরে ভুল প্রমাণিত হয়েছে। এই কারণেই machine-checked proof (Coq, Isabelle) এত মূল্যবান।
তবু: প্রমাণ থাকা আর না থাকার মধ্যে পার্থক্য বিশাল। CompCert-এর verified অংশে শূন্য miscompilation bug — এটা কাকতালীয় নয়।
“প্রমাণ academic জিনিস, industry-তে কেউ করে না।”
Formal proof লেখা বিরল, সত্যি। কিন্তু proof-এর চিন্তাধারা সর্বত্র:
- একটা code review-তে “এই condition কি সব ক্ষেত্রে ঠিক?” — proof thinking
- একটা edge case ধরা — counterexample খোঁজা
- “এই loop কি সবসময় শেষ হবে?” — termination argument
- Type system compile-time-এ যা যাচাই করে — automated proof
- একটা design doc-এ “কেন এটা কাজ করবে” অংশ — অনানুষ্ঠানিক proof
আর যেসব ক্ষেত্রে ভুলের দাম অসহনীয় — kernel, compiler, crypto, aerospace, medical device, financial infrastructure — সেখানে formal proof ক্রমশ বাধ্যতামূলক হচ্ছে।
“একটা দাবি প্রমাণ করতে না পারা মানে সেটা মিথ্যা।”
না। তিনটা আলাদা অবস্থা:
- দাবিটা সত্য, প্রমাণ আছে
- দাবিটা মিথ্যা, counterexample আছে
- জানি না — প্রমাণও নেই, counterexample-ও নেই
তৃতীয় অবস্থাটাই গণিতের বেশিরভাগ সময়ের অবস্থা। Collatz conjecture, Goldbach conjecture, P vs NP — সবই এই দলে।
আর Gödel দেখিয়েছেন কিছু দাবি আছে যা সত্য কিন্তু প্রমাণ করা যায় না (যেকোনো নির্দিষ্ট formal system-এ)।
Debugging-এ এটা মনে রাখা জরুরি: “আমি bug-টা reproduce করতে পারছি না” মানে “bug নেই” নয়।
বুঝেছেন কি না দেখুন
1প্রমাণ করুন: 3n + 2 বিজোড় হলে n বিজোড়। কোন technique বেছে নিলেন
এবং কেন?
প্রয়োগ
3n + 2 বিজোড় হলে n বিজোড়। কোন technique বেছে নিলেন
এবং কেন?Contrapositive বেছে নেব: “n জোড় হলে 3n + 2 জোড়।”
কারণ direct proof-এ শুরু করতে হতো “3n + 2 = 2k + 1” থেকে, তারপর
n সম্পর্কে কিছু বের করতে হতো — সেটা ঘুরপথ। Contrapositive-এ
n-এর সংজ্ঞা থেকে সরাসরি শুরু করা যায়।
প্রমাণ (contrapositive). ধরি n জোড়, অর্থাৎ n = 2k কোনো
পূর্ণসংখ্যা k-এর জন্য।
3k + 1 পূর্ণসংখ্যা, তাই 3n + 2 জোড়।
Contrapositive প্রমাণিত, অতএব মূল দাবিও প্রমাণিত। ∎
সংকেতটা কীভাবে চিনবেন: hypothesis-এ (3n+2 বিজোড়) একটা যৌগিক
রাশি আছে, conclusion-এ (n বিজোড়) একটা সরল রাশি। উল্টে দিলে সরলটা
hypothesis হয়ে যায় — আর সরল hypothesis থেকে কাজ শুরু করা সবসময় সহজ।
2এই “প্রমাণ”-টার ভুল ধরুন:
দাবি: সব ঘোড়া একই রঙের।
প্রমাণ (n সংখ্যক ঘোড়ার সেটের উপর induction).
Base: ১টা ঘোড়ার সেটে সব ঘোড়া একই রঙের ✓
Step: ধরি n ঘোড়ার যেকোনো সেটে সব একই রঙের। এবার n+1 ঘোড়ার
একটা সেট নিন। প্রথম n টা নিলে তারা একই রঙের। শেষ n টা নিলে
তারাও একই রঙের। দুইটা সেটে overlap আছে, তাই সবাই একই রঙের ∎
যুক্তি
দাবি: সব ঘোড়া একই রঙের।
প্রমাণ (n সংখ্যক ঘোড়ার সেটের উপর induction).
Base: ১টা ঘোড়ার সেটে সব ঘোড়া একই রঙের ✓
Step: ধরি n ঘোড়ার যেকোনো সেটে সব একই রঙের। এবার n+1 ঘোড়ার
একটা সেট নিন। প্রথম n টা নিলে তারা একই রঙের। শেষ n টা নিলে
তারাও একই রঙের। দুইটা সেটে overlap আছে, তাই সবাই একই রঙের ∎
ভুলটা n = 1 থেকে n = 2-তে যাওয়ার ধাপে।
n + 1 = 2 ঘোড়া মানে {h₁, h₂}।
- “প্রথম
n = 1টা” ={h₁} - “শেষ
n = 1টা” ={h₂}
এই দুইটা সেটের কোনো overlap নেই। তাই “overlap-এর ঘোড়াটার মাধ্যমে দুই দল সংযুক্ত” — এই যুক্তিটা এখানে খাটে না।
n ≥ 2 -এর জন্য overlap থাকে, তাই argument-টা তখন বৈধ। কিন্তু
induction-এর শৃঙ্খল n = 1 -এ ভেঙে গেছে, তাই কখনোই n = 2-তে
পৌঁছানো যায় না — আর সেখান থেকে উপরেও ওঠা যায় না।
সাধারণ শিক্ষা: inductive step-এ যদি একটা অনুমান লুকিয়ে থাকে
(এখানে “overlap আছে”, যা n ≥ 2 দাবি করে), তাহলে সেই অনুমানটা
base case থেকে শুরু করেই সত্য হতে হবে।
এই ধরনের ভুল induction-এর সবচেয়ে সাধারণ ফাঁদ, আর পরের লেসনে আমরা এটা এড়ানোর নিয়মতান্ত্রিক পদ্ধতি দেখব।
কোডে এর সমতুল্য: একটা recursive function যার base case
n == 0 কিন্তু recursive case n == 1 -এ f(n-2) ডাকে —
শৃঙ্খলটা কখনো base-এ পৌঁছায় না।
3আপনার cache eviction policy: “সবচেয়ে কম সম্প্রতি ব্যবহৃত entry বাদ দাও।”
প্রমাণ করুন (বা খণ্ডন করুন): এই policy সবসময় সর্বোচ্চ hit rate দেয়।
ডিজাইন
খণ্ডন — counterexample দিয়ে।
Cache-এর ধারণক্ষমতা ২। Access sequence:
A, B, C, A, B, C, A, B, C, …LRU-র আচরণ:
| Access | Cache আগে | ফল | Cache পরে |
|---|---|---|---|
| A | [] | miss | [A] |
| B | [A] | miss | [A, B] |
| C | [A, B] | miss, A বাদ | [B, C] |
| A | [B, C] | miss, B বাদ | [C, A] |
| B | [C, A] | miss, C বাদ | [A, B] |
| C | [A, B] | miss, A বাদ | [B, C] |
১০০% miss — প্রতিবার ঠিক সেই জিনিসটা বাদ দেওয়া হয় যেটা পরেই লাগবে।
একটা ভালো policy: সবসময় A আর B রাখুন, C কখনো cache করবেন না।
তাহলে ৩টার মধ্যে ২টা hit — ৬৬% hit rate।
অতএব LRU সর্বোচ্চ নয়। ∎
তাত্ত্বিক সীমা — Bélády’s optimal algorithm (OPT): সেই entry বাদ দিন যেটা সবচেয়ে দূর ভবিষ্যতে লাগবে। এটা প্রমাণিতভাবে optimal, কিন্তু ভবিষ্যৎ জানা লাগে — তাই বাস্তবে অসম্ভব।
তাহলে LRU কেন ব্যবহার হয়? কারণ বাস্তব access pattern-এ temporal locality থাকে — সম্প্রতি ব্যবহৃত জিনিস আবার লাগার সম্ভাবনা বেশি। LRU সেই অনুমানের উপর ভালো কাজ করে।
আর এখানেই একটা গুরুত্বপূর্ণ পার্থক্য:
| দাবি | |
|---|---|
| প্রমাণযোগ্য | “LRU সব sequence-এ optimal” — মিথ্যা |
| প্রমাণযোগ্য | “LRU-র competitive ratio k” (k = cache size) — সত্য |
| অভিজ্ঞতালব্ধ | “বাস্তব workload-এ LRU ভালো” — measurement-এর বিষয় |
Engineering-এ তিনটাই দরকার, কিন্তু গুলিয়ে ফেলা যাবে না।
Level 3 (cache) আর Level 8 (buffer pool)-এ আমরা এই policy-গুলো বিস্তারিত দেখব — এবং measure করব।
4Pigeonhole principle ব্যবহার করে প্রমাণ করুন: ঢাকা শহরে অন্তত দুইজন
মানুষ আছে যাদের মাথায় ঠিক একই সংখ্যক চুল আছে।
যুক্তি
প্রমাণ.
কবুতর: ঢাকার মানুষ। জনসংখ্যা প্রায় ২ কোটি (2 × 10⁷)।
খোপ: সম্ভাব্য চুলের সংখ্যা। মানুষের মাথায় সাধারণত ১ লক্ষ থেকে
১.৫ লক্ষ চুল থাকে; একটা উদার উপরের সীমা ধরি ১০ লক্ষ (10⁶)।
তাহলে সম্ভাব্য মান 0 থেকে 10⁶, অর্থাৎ 10⁶ + 1 টা খোপ।
যেহেতু 2 × 10⁷ > 10⁶ + 1, pigeonhole অনুযায়ী অন্তত দুইজন একই খোপে। ∎
আসলে আরো শক্ত কিছু বলা যায়: generalized pigeonhole অনুযায়ী
অন্তত ⌈2×10⁷ / (10⁶+1)⌉ = 20 জনের চুলের সংখ্যা অভিন্ন।
এই প্রমাণটা কী দেখায়: আমরা কারো মাথার চুল গুনিনি, কোনো ডেটা সংগ্রহ করিনি — তবু নিশ্চিতভাবে একটা সত্য প্রতিষ্ঠা করেছি। এটাই counting argument-এর শক্তি।
CS-এ একই যুক্তির প্রয়োগ:
- ৩২-bit hash-এ
2³²টা সম্ভাব্য মান।2³² + 1টা distinct input দিলে collision নিশ্চিত। - Birthday paradox:
√(2³²) ≈ 65536টা input-এই ৫০% সম্ভাবনায় collision। এটা pigeonhole-এর probabilistic সংস্করণ, পরের লেসনে দেখব। - একটা
n-bit counter সর্বোচ্চ2ⁿটা ভিন্ন অবস্থা রাখতে পারে;2ⁿ + 1বার বাড়ালে অবশ্যই পুনরাবৃত্তি — অর্থাৎ overflow বা wraparound অনিবার্য। - যেকোনো সসীম-state machine যদি অসীমকাল চলে, তাহলে অবশ্যই একটা state-এ ফিরে আসবে — অর্থাৎ চক্রে পড়বে। এটাই cycle detection-এর ভিত্তি।
5এই function-টার correctness প্রমাণ করুন — বা একটা counterexample দিন।
def is_power_of_two(n):
return n > 0 and (n & (n - 1)) == 0
প্রয়োগ
def is_power_of_two(n):
return n > 0 and (n & (n - 1)) == 0দাবি: এই function True ফেরত দেয় ঠিক তখনই যখন n = 2ᵏ কোনো
k ≥ 0-এর জন্য।
প্রমাণ, দুই দিকে।
(⟸) n দুইয়ের ঘাত হলে function True দেয়।
n = 2ᵏ মানে binary-তে n-এর ঠিক একটা bit সেট — position k-তে।
n = 1 0 0 0 (k = 3, অর্থাৎ 8)
n - 1 = 0 1 1 1 (7)কেন? 1000 থেকে 1 বিয়োগ করলে সবচেয়ে ডানের সেট bit 0 হয় আর
তার ডানের সব bit 1 হয়। এখানে সেট bit-টাই position k-তে, তাই
সেটা 0 হয় আর নিচের সব bit 1 হয়।
ফলে n আর n−1-এর কোনো position-এ একসাথে 1 নেই:
1 0 0 0
0 1 1 1
─────── AND
0 0 0 0n & (n-1) == 0 ✓ আর n > 0 ✓
(⟹) Function True দিলে n দুইয়ের ঘাত।
Contrapositive প্রমাণ করি: n > 0 কিন্তু n দুইয়ের ঘাত নয় হলে
n & (n-1) ≠ 0।
n দুইয়ের ঘাত না হলে তার binary-তে অন্তত দুইটা bit সেট।
ধরি সবচেয়ে ডানের সেট bit position j-তে, আর তার উপরে আরো অন্তত
একটা সেট bit আছে position m > j-তে।
n − 1 করলে: position j-এর bit 0 হয়, j-এর নিচের সব bit 1 হয়,
আর j-এর উপরের সব bit অপরিবর্তিত থাকে।
তাই position m-এ n আর n−1 দুটোতেই 1 আছে। AND করলে সেখানে 1
থাকবে, অর্থাৎ ফল শূন্য নয়। ∎
Edge case যাচাই:
n | n & (n-1) | Function | সঠিক? |
|---|---|---|---|
1 (2⁰) | 1 & 0 = 0 | True | ✓ |
| 2 | 10 & 01 = 0 | True | ✓ |
| 3 | 11 & 10 = 10 | False | ✓ |
| 0 | — | False (n > 0 ব্যর্থ) | ✓ |
| −8 | — | False | ✓ |
n = 0 -এর ক্ষেত্রটা লক্ষ্য করুন: 0 & (0-1) = 0 & -1 = 0, তাই
n > 0 guard না থাকলে function ভুলভাবে True দিত। এটাই সেই
“অনুচ্চারিত precondition” যা প্রমাণ লিখতে গিয়ে সামনে আসে।
Level 1-এ আমরা bit manipulation-এর এই কৌশলগুলো বিস্তারিত দেখব —
কেন n & (n-1) সবচেয়ে ডানের সেট bit মোছে, আর সেটা দিয়ে আর কী কী করা যায়।
এরপর কী
আমাদের হাতে এখন পাঁচটা হাতিয়ার আছে। কিন্তু একটা গুরুত্বপূর্ণ শ্রেণির দাবি এখনো ধরা যাচ্ছে না।
কীভাবে প্রমাণ করবেন যে একটা recursive function সব input-এ কাজ করে? বা একটা loop সব iteration-এ invariant রক্ষা করে? বা একটা tree-র সব node-এ একটা property খাটে?
এসব দাবিতে অসীম সংখ্যক ক্ষেত্র আছে, আর direct proof একটা একটা করে সেগুলো ঢাকতে পারে না।
পরের লেসনে আসছে mathematical induction — একমাত্র হাতিয়ার যা অসীম সংখ্যক ক্ষেত্র সসীম যুক্তিতে ঢাকতে পারে। Weak induction, strong induction, structural induction — আর সবচেয়ে গুরুত্বপূর্ণ: recursion আর induction যে আসলে একই জিনিসের দুইটা দিক, সেটা।
আরও পড়ুন
- How to Prove It — A Structured Approach — Daniel Velleman · প্রমাণ লেখা শেখার সবচেয়ে ভালো বই, তুলনাহীন
- Mathematics for Computer Science, Chapter 1 — Lehman, Leighton, Meyer