Lambda Calculus — তিনটা নিয়মে সব গণনা

আগে এটা বুঝি

১৯৩৬ সাল। কোনো ইলেকট্রনিক কম্পিউটার তখনও তৈরি হয়নি — ENIAC-এর জন্মের আরও আট বছর বাকি। অথচ Princeton-এর গণিতবিদ Alonzo Church একটা প্রশ্নের উত্তর দিচ্ছেন: “গণনা” (computation) বলতে গাণিতিকভাবে ঠিক কী বোঝায়?

Church-এর উত্তর আশ্চর্যজনকভাবে ছোট। মাত্র তিনটা জিনিস দিয়ে একটা ভাষা:

একটা variable (x)
একটা function বানানোর নিয়ম (λx. ...) — “abstraction”
একটা function প্রয়োগ করার নিয়ম (f a) — “application”

আর মাত্র একটা reduction rule — একটা function-কে তার argument-এ প্রয়োগ করলে কী হয় সেটা বর্ণনা করার নিয়ম।

এতটুকুই। কোনো সংখ্যা নেই, কোনো if নেই, কোনো loop নেই, কোনো তালিকা নেই। অথচ Church (এবং একই সময়ে, স্বাধীনভাবে, Alan Turing তার machine দিয়ে) প্রমাণ করলেন — এই তিনটা জিনিস দিয়েই যা কিছু গণনাযোগ্য, সব গণনা করা যায়। সংখ্যা, boolean, তালিকা, এমনকি recursion — সবকিছু এই তিনটা primitive দিয়েই বানানো যায়, “built-in” হিসেবে কিছুই লাগে না।

cs-theory/turing-machines-এ আমরা দেখেছি একটা tape, head, আর transition table দিয়ে গণনার একটা model। Lambda calculus সম্পূর্ণ ভিন্ন দর্শন থেকে একই গন্তব্যে পৌঁছায় — কোনো state নেই, কোনো memory নেই, শুধু function-এর উপর function প্রয়োগ। দুইটা মডেল, একই ক্ষমতা — এটাই cs-theory-র Church-Turing thesis লেসনের কেন্দ্রীয় দাবি।

এই লেসনের শেষে আপনি দেখবেন এই “খেলনা” ক্যালকুলাস আজও জীবিত — প্রতিটা Python lambda, প্রতিটা JavaScript arrow function, আর পুরো Haskell ভাষা আক্ষরিক অর্থে এই একই তিনটা নিয়মের উপর দাঁড়িয়ে।

মূল ধারণা

Syntax — তিনটা নিয়মে একটা ব্যাকরণ

Lambda calculus-এর পুরো গ্রামার (BNF):

e ::= x           (variable)
    | λx. e        (abstraction — একটা ফাংশন সংজ্ঞা)
    | e1 e2        (application — একটা ফাংশন প্রয়োগ)

একটা e-কে বলা হয় একটা term (বা expression)।

Abstraction — নামহীন ফাংশন

λx. e মানে “একটা ফাংশন যা x নেয়, আর e ফেরত দেয়”। আধুনিক notation-এ:

λx. x        ≈  x => x                (identity function, Python-এ lambda x: x)
λx. x + 1    ≈  x => x + 1

লক্ষ্য করুন — ফাংশনের কোনো নাম নেই। λx. x নিজেই একটা মান, সরাসরি ব্যবহারযোগ্য বা আরেকটা ফাংশনে পাস করার যোগ্য। এটাই “anonymous function”/“lambda” শব্দের আক্ষরিক উৎস।

Application — প্রয়োগ

e1 e2 মানে “e1-কে e2-এর উপর প্রয়োগ করা”। Application বাম-সংযোজী (left-associative):

f a b c   মানে   ((f a) b) c

Currying — সব ফাংশন এক-argument

লক্ষ্য করুন গ্রামারে multi-argument abstraction নেই — শুধু λx. e, একটা মাত্র variable। দুই বা তিন argument-এর ফাংশন বানাতে nested abstraction ব্যবহার হয়:

$\lambda x.\, \lambda y.\, x + y$

এটা “দুই argument-এর একটা ফাংশন” না — এটা “একটা x নেয়, আর ফেরত দেয় আরেকটা ফাংশন যেটা y নেয়”। (λx. λy. x+y) 3 4 ধাপে ধাপে: প্রথমে 3 প্রয়োগ হয়ে λy. 3+y পাওয়া যায় (একটা নতুন ফাংশন!), তারপর 4 প্রয়োগ হয়ে 3+4 = 7।

Parenthesization convention

দুইটা নিয়ম মনে রাখলেই যথেষ্ট:

Application বাম-সংযোজী: f a b = (f a) b, (a (b c)) নয়
Abstraction-এর body যতদূর সম্ভব ডানে বিস্তৃত হয়: λx. x y মানে λx. (x y), (λx. x) y নয়

λx. λy. x y z   ≡   λx. (λy. ((x y) z))

মূল ধারণা

Beta reduction — একমাত্র computation rule

পুরো lambda calculus-এর “চলা” মানে একটাই নিয়ম প্রয়োগ করা: beta reduction।

$(\lambda x.\, e)\ a\ \ \longrightarrow\ \ e[a/x]$

মানে: “λx.e-কে a-এর উপর প্রয়োগ করলে, e-এর ভেতর প্রতিটা free x-কে a দিয়ে replace করো।” এই (λx.e) a আকারের subterm-কে বলা হয় একটা redex (reducible expression)।

উদাহরণ ১ — সরাসরি

$(\lambda x.\, x)\ 5 \ \longrightarrow\ 5$

Identity function 5-এর উপর প্রয়োগ — সরাসরি 5 ফেরত।

উদাহরণ ২ — দুই ধাপ, currying-সহ

$(\lambda x.\, \lambda y.\, x)\ a\ b$

Application বাম-সংযোজী, তাই এটা ((λx.λy.x) a) b।

ধাপ ১: (λx.λy.x) a — বাইরের redex, x-কে a দিয়ে replace:

$\longrightarrow\ \lambda y.\, a$

ধাপ ২: (λy. a) b — y কোথাও নেই body-তে, তাই কিছুই বদলায় না:

$\longrightarrow\ a$

লক্ষ্য করুন — b টা সম্পূর্ণ উপেক্ষিত হলো! এই term-টাকেই আমরা পরে TRUE (Church boolean) হিসেবে চিনব — “দুইটা জিনিস দাও, প্রথমটা ফেরত দাও।”

Redex, normal form, আর non-termination

একটা term-কে বলা হয় normal form-এ যখন তাতে আর কোনো redex নেই — আর কোনো beta reduction প্রয়োগ করা যায় না। সব term কি normal form-এ পৌঁছায়?

না। বিখ্যাত পাল্টা-উদাহরণ:

$\Omega \;=\; (\lambda x.\, x\, x)\ (\lambda x.\, x\, x)$

Reduce করুন: x-কে (λx.xx) দিয়ে replace করলে ঠিক একই term ফেরত আসে:

$(\lambda x.\,x\,x)\,(\lambda x.\,x\,x) \ \longrightarrow\ (\lambda x.\,x\,x)\,(\lambda x.\,x\,x) \ \longrightarrow\ \cdots$

Ω চিরকাল নিজের মধ্যে reduce হতে থাকে, কখনো normal form-এ পৌঁছায় না — lambda calculus-এর একটা infinite loop। এটা আকস্মিক নয় — cs-theory-র halting problem লেসনে যা দেখেছেন তার সরাসরি প্রতিফলন: যদি lambda calculus Turing-সমতুল্য হয় (নিচে দেখব), তাহলে “একটা term normal form-এ পৌঁছায় কি না” প্রশ্নটাও undecidable হতেই হবে — আর Ω তারই একটা concrete সাক্ষী।

Reduction order কখনো কখনো গুরুত্বপূর্ণ

(λx. y) Ω বিবেচনা করুন — একটা ফাংশন যে তার argument সম্পূর্ণ উপেক্ষা করে। যদি প্রথমে argument reduce করার চেষ্টা করেন (applicative order, “eager”), Ω-এ আটকে যাবেন চিরকাল। কিন্তু যদি প্রথমে বাইরের redex reduce করেন (normal order, “lazy”), সরাসরি y পাবেন — Ω কখনো স্পর্শই করা হবে না!

এই পার্থক্যটাই programming-languages/evaluation-strategies-এর call-by-value বনাম call-by-name-এর গাণিতিক উৎস। Standardization theorem বলে: যদি একটা term-এর কোনো normal form থাকে, normal-order reduction সেটা সবসময় খুঁজে পাবে — applicative order অনেক সময় পায় না।

মূল ধারণা

Free ও bound variable, আর alpha conversion

λx. e-তে x-কে বলা হয় bound — এটা এই abstraction-এর “প্যারামিটার”, বাইরের জগতের সাথে সম্পর্কহীন। যে variable কোনো λ-এর বাঁধনে নেই, তাকে বলে free।

λx. x y     ← x bound (λx বেঁধেছে), y free
λx. λy. x y ← x ও y দুটোই bound
x (λy. y)   ← x free, y bound

কেন গুরুত্বপূর্ণ? কারণ bound variable-এর নাম গুরুত্বহীন — শুধু তার “কোন λ-এর সাথে বাঁধা” সেটাই অর্থপূর্ণ। λx. x আর λz. z — দুটোই ঠিক একই ফাংশন (identity), শুধু bound variable-এর নাম আলাদা। এই পুনর্নামকরণকে বলে alpha conversion:

$\lambda x.\, e \;\equiv_\alpha\; \lambda z.\, e[z/x] \qquad (\text{যদি } z \text{ } e\text{-তে free না থাকে})$

Variable capture — যেখানে naive substitution ভেঙে পড়ে

এই শর্তটা (“z free না থাকা”) তুচ্ছ মনে হতে পারে, কিন্তু এটা বাদ দিলে বিপর্যয় ঘটে। বিবেচনা করুন:

$(\lambda x.\, \lambda y.\, x)\ y$

আমরা চাই — λx. λy. x-এর body-তে x-এর জায়গায় (বাইরের, free) y বসানো। কিন্তু body হলো λy. x — এখানে একটা নতুন, bound y আছে! যদি সরলভাবে substitute করি:

$\lambda y.\, x \;\; [y/x] \;\; \stackrel{\text{ভুল!}}{=} \;\; \lambda y.\, y$

এটা ভয়ানক ভুল — বাইরের free y-টা এখন ভেতরের λy-এর সাথে “capture” হয়ে গেছে, মানে ভুলভাবে bound হয়ে গেল। মূল অর্থ ছিল “প্রথম argument ফেরত দাও” (TRUE-এর মতো); ভুল substitution-এর পর এটা হয়ে গেছে “identity function”।

সমাধান — capture-avoiding substitution: প্রতিস্থাপনের আগে, ভেতরের bound variable-টা alpha-convert করে অন্য নাম দিন:

$\lambda y.\, x \;\equiv_\alpha\; \lambda w.\, x \quad\Longrightarrow\quad (\lambda w.\, x)[y/x] = \lambda w.\, y \;\; \checkmark$

এখন সঠিক ফলাফল — বাইরের y অক্ষত থাকল, ভেতরের bound variable-এর নাম বদলে গেল।

ধাপ	Term	ব্যাখ্যা
শুরু	`(λx. λy. x) y`	Outer `y` free, inner `y` bound — একই নাম, ভিন্ন identity
Naive substitute	`λy. y`	ভুল — free `y` capture হয়ে গেছে
Alpha-rename প্রথমে	`(λx. λw. x) y`	Inner bound variable-এর নাম বদলানো, অর্থ অপরিবর্তিত
তারপর substitute	`λw. y`	সঠিক — ফাংশনটা এখনও “প্রথম argument ফেরত দাও”

Capture-avoiding substitution — alpha conversion না করলে ভুল অর্থ তৈরি হয়।

বাস্তব interpreter-এ কীভাবে এড়ানো হয়

বাস্তব compiler/interpreter (compilers/lexical-analysis-এর পরবর্তী ধাপগুলো, semantic analysis) সাধারণত variable নাম নিয়েই কাজ করে না — De Bruijn index ব্যবহার করে, যেখানে প্রতিটা variable-কে তার ঘিরে-থাকা λ-এর সংখ্যা দিয়ে (নাম না দিয়ে) নির্দেশ করা হয়। এতে alpha conversion সম্পূর্ণ অপ্রয়োজনীয় হয়ে যায় — দুইটা “alpha-equivalent” term একদম identical bit-pattern হয়ে দাঁড়ায়। একই সমস্যা (hygiene) macro system-এও দেখা যায় — Scheme-এর hygienic macro ব্যবস্থা মূলত এই একই capture সমস্যার সমাধান, ভিন্ন context-এ।

ভেতরে কী ঘটছে

Church Encoding — শুধু ফাংশন দিয়ে ডেটা বানানো

এখানেই lambda calculus-এর সবচেয়ে চমকপ্রদ দিকটা দেখা যায়: এতে কোনো true/false, কোনো pair, কোনো সংখ্যা built-in নেই — অথচ এগুলো সব শুধু function দিয়েই এনকোড করা যায়।

Boolean

$\text{TRUE} = \lambda x.\, \lambda y.\, x \qquad\qquad \text{FALSE} = \lambda x.\, \lambda y.\, y$

লক্ষ্য করুন — TRUE ঠিক আগের উদাহরণের সেই (λx.λy.x) term। এই সংজ্ঞা থেকেই IF তৈরি হয়:

$\text{IF} = \lambda b.\, \lambda t.\, \lambda f.\, b\ t\ f$

কেন এটা কাজ করে? যদি b = TRUE, তাহলে b t f = TRUE t f = (λx.λy.x) t f, যা reduce হয়ে সরাসরি t দেয় (ঠিক যেমন আমরা আগে হাতে দেখিয়েছি)। যদি b = FALSE, b t f reduce হয়ে f দেয়। কোনো “if-then-else” primitive লাগেনি — শুধু function application-এর মধ্যেই branching লুকিয়ে আছে।

চলুন IF TRUE a b সম্পূর্ণ reduce করি:

\begin{aligned} \text{IF}\ \text{TRUE}\ a\ b &= (\lambda b.\lambda t.\lambda f.\, b\,t\,f)\ \text{TRUE}\ a\ b \\ &\longrightarrow (\lambda t.\lambda f.\, \text{TRUE}\,t\,f)\ a\ b \\ &\longrightarrow (\lambda f.\, \text{TRUE}\,a\,f)\ b \\ &\longrightarrow \text{TRUE}\ a\ b \\ &= (\lambda x.\lambda y.\,x)\ a\ b \ \longrightarrow\ (\lambda y.\, a)\ b\ \longrightarrow\ a \end{aligned}

পাঁচটা beta reduction, কোনো special-case machinery ছাড়া — শুধু substitution, বারবার।

Pair

$\text{PAIR} = \lambda x.\, \lambda y.\, \lambda f.\, f\,x\,y \qquad \text{FIRST} = \lambda p.\, p\ \text{TRUE} \qquad \text{SECOND} = \lambda p.\, p\ \text{FALSE}$

PAIR a b একটা function যেটা তার নিজের “selector” গ্রহণ করে। FIRST (PAIR a b):

$\text{FIRST}\ (\text{PAIR}\ a\ b) = (\lambda p.\,p\,\text{TRUE})\ (\lambda f.\,f\,a\,b) \longrightarrow (\lambda f.\,f\,a\,b)\ \text{TRUE} \longrightarrow \text{TRUE}\ a\ b \longrightarrow a$

PAIR-এর ভেতর a আর b-কে কোথাও storage-এ রাখা হয়নি — তারা শুধু একটা ফাংশনের closed-over variable, যা পরে সঠিক selector দিয়ে বের করা যায়। এটাই মূলত programming-languages/closures-and-environments-এ দেখা “code + captured environment” জোড়ার একদম বিশুদ্ধ রূপ।

উদাহরণ

Church numeral — সংখ্যাও শুধু function

একটা সংখ্যা n-কে এনকোড করা হয় “একটা function-কে n বার প্রয়োগ করার” ক্ষমতা হিসেবে:

\begin{aligned} 0 &= \lambda f.\, \lambda x.\, x \\ 1 &= \lambda f.\, \lambda x.\, f\,x \\ 2 &= \lambda f.\, \lambda x.\, f\,(f\,x) \\ 3 &= \lambda f.\, \lambda x.\, f\,(f\,(f\,x)) \\ n &= \lambda f.\, \lambda x.\, \underbrace{f\,(f\,(\cdots f}_{n\text{ বার}}\,x)\cdots) \end{aligned}

0 হলো FALSE-এর মতোই দেখতে (λx.λy.y বনাম λf.λx.x) — কাকতালীয় না, দুটোই “দ্বিতীয় argument সরাসরি ফেরত দাও” প্যাটার্ন।

Successor — এক যোগ করা

$\text{SUCC} = \lambda n.\, \lambda f.\, \lambda x.\, f\ (n\ f\ x)$

মানে: “n-কে f আর x দিয়ে চালাও (যা f-কে n বার প্রয়োগ করবে), তারপর ফলাফলে আরেকবার f প্রয়োগ করো।”

চলুন SUCC 0 reduce করে যাচাই করি এটা 1-এর সমান কি না:

\begin{aligned} \text{SUCC}\ 0 &= (\lambda n.\lambda f.\lambda x.\, f\,(n\,f\,x))\ (\lambda f.\lambda x.\,x) \\ &\longrightarrow \lambda f.\lambda x.\, f\,\big((\lambda f.\lambda x.\,x)\ f\ x\big) \\ &\longrightarrow \lambda f.\lambda x.\, f\,(x) \qquad [(\lambda f.\lambda x.x)\ f\ x \to x, \text{ ভেতরের } f,x \text{ প্রয়োগে}] \\ &= \lambda f.\lambda x.\, f\,x \end{aligned}

এটাই ঠিক 1-এর সংজ্ঞা। ✓

Addition

$\text{PLUS} = \lambda m.\, \lambda n.\, \lambda f.\, \lambda x.\, m\ f\ (n\ f\ x)$

মানে: “n-কে f,x-এর উপর চালিয়ে একটা ফলাফল পাও, তারপর তার উপরে m-কে f প্রয়োগ করতে থাকো।” PLUS 1 1-এর reduction ধারণাগতভাবে: n f x প্রথমে f x দেয় (যেহেতু n=1), তারপর m f (f x) মানে 1-কে f-এর সাথে সেই f x-এর উপর চালানো — f (f x), যা ঠিক Church numeral 2।

Recursion ছাড়া recursion — Y combinator

একটা সমস্যা থেকে যায়: lambda calculus-এ কোনো নাম নেই (সব anonymous), তাহলে একটা ফাংশন নিজেকে কীভাবে কল করবে (recursion)? সমাধান — fixed-point combinator:

$Y = \lambda f.\, (\lambda x.\, f\,(x\,x))\, (\lambda x.\, f\,(x\,x))$

Y g reduce করলে g (Y g) পাওয়া যায় — অর্থাৎ Y g নিজেই তার “এক ধাপ আরও প্রসারিত” রূপের সমান। এভাবে g-কে একটা non-recursive ফাংশন হিসেবে লিখে (যা তার “নিজেকে” একটা parameter হিসেবে নেয়), Y g দিয়ে সত্যিকারের recursive আচরণ তৈরি করা যায় — নাম ছাড়াই। mathematics/induction-এর “recursive leap of faith” ধারণাটাই এখানে আক্ষরিক গাণিতিক রূপ পেল।

নিজে চালিয়ে দেখুন

EXPERIMENT

Python-এ lambda calculus চালানো — Church encoding সত্যিই কাজ করে দেখা

Python 3 (কোনো library লাগে না)· ২০ মিনিট

# ── Church booleans ──────────────────────────────────────────────
TRUE  = lambda x: lambda y: x
FALSE = lambda x: lambda y: y
IF    = lambda b: lambda t: lambda f: b(t)(f)

# ── Church pairs ─────────────────────────────────────────────────
PAIR   = lambda x: lambda y: lambda f: f(x)(y)
FIRST  = lambda p: p(TRUE)
SECOND = lambda p: p(FALSE)

# ── Church numerals ──────────────────────────────────────────────
ZERO = lambda f: lambda x: x
def SUCC(n):
    return lambda f: lambda x: f(n(f)(x))

def PLUS(m):
    return lambda n: lambda f: lambda x: m(f)(n(f)(x))

def MULT(m):
    return lambda n: lambda f: m(n(f))

# ── Church numeral ↔ Python int, শুধু পড়ার সুবিধার জন্য ──────────
def to_int(church_n):
    return church_n(lambda k: k + 1)(0)

def from_int(n):
    result = ZERO
    for _ in range(n):
        result = SUCC(result)
    return result


# ── যাচাই ─────────────────────────────────────────────────────────
print("TRUE বেছে নেয় প্রথমটা :", IF(TRUE)("HEAD")("TAIL"))
print("FALSE বেছে নেয় দ্বিতীয়টা:", IF(FALSE)("HEAD")("TAIL"))

p = PAIR(10)(20)
print("FIRST(PAIR(10,20)) =", FIRST(p))
print("SECOND(PAIR(10,20)) =", SECOND(p))

three = from_int(3)
four  = SUCC(three)
print("SUCC(3) =", to_int(four))

two  = from_int(2)
five = PLUS(two)(three)
print("PLUS(2,3) =", to_int(five))

six = MULT(two)(three)
print("MULT(2,3) =", to_int(six))

প্রত্যাশিত আউটপুট:

TRUE বেছে নেয় প্রথমটা : HEAD
FALSE বেছে নেয় দ্বিতীয়টা: TAIL
FIRST(PAIR(10,20)) = 10
SECOND(PAIR(10,20)) = 20
SUCC(3) = 4
PLUS(2,3) = 5
MULT(2,3) = 6

যা এখানে গুরুত্বপূর্ণ: পুরো প্রোগ্রামে কোথাও if, True/False, tuple, বা built-in int arithmetic ব্যবহৃত হয়নি (শুধু to_int/ from_int কনভার্টারে, পড়ার সুবিধার জন্য) — TRUE/FALSE/PAIR/সংখ্যা সবকিছু নিছক ফাংশন, আর তাদের আচরণ নিছক function application-এ লুকিয়ে আছে। Python-এর একমাত্র যে feature-টা এখানে আসলে দরকার হলো closure — একটা inner lambda তার ঘিরে-থাকা variable (n, x, y) মনে রাখতে পারে, ঠিক lambda calculus-এর free variable capture যেভাবে কাজ করে।

এটা কী প্রমাণ করে

Python-এর lambda শুধু একটা syntax sugar না — Church encoding-এর প্রতিটা নিয়ম আক্ষরিকভাবে চালানো যায়, শুধু একটা মাত্র feature (single-argument function + closure) দিয়ে, কোনো built-in boolean/integer ছাড়াই।

নিজে বানান

BUILD IT

একটা মিনিয়েচার beta-reducer লেখা

Python · ●●●●○

Term-এর তিনটা variant (Var, Abs, App) একটা tagged data structure হিসেবে define করুন
Substitution function লিখুন — capture এড়াতে alpha-rename করুন যখন দরকার
একটা single-step beta-reduce function লিখুন — বাইরের redex খুঁজে reduce করুন (normal order)
পুরো normal form পাওয়া পর্যন্ত repeat করুন, একটা step-limit সহ (Ω-এর মতো term-এর জন্য)

লক্ষ্য: lambda calculus-এর reduction নিয়মগুলো শুধু “বোঝা” না, সত্যিই চালিয়ে দেখা — যাতে variable capture, normal order, আর non-termination আক্ষরিক কোডে দেখা যায়।

import itertools

counter = itertools.count()
def fresh(base="v"):
    return f"{base}{next(counter)}"


class Var:
    def __init__(self, name): self.name = name
    def __repr__(self): return self.name

class Abs:
    def __init__(self, param, body): self.param, self.body = param, body
    def __repr__(self): return f"(\\{self.param}. {self.body})"

class App:
    def __init__(self, fn, arg): self.fn, self.arg = fn, arg
    def __repr__(self): return f"({self.fn} {self.arg})"


def free_vars(t):
    if isinstance(t, Var):
        return {t.name}
    if isinstance(t, Abs):
        return free_vars(t.body) - {t.param}
    if isinstance(t, App):
        return free_vars(t.fn) | free_vars(t.arg)


def substitute(t, name, value):
    """t[value/name] — capture-avoiding।"""
    if isinstance(t, Var):
        return value if t.name == name else t
    if isinstance(t, App):
        return App(substitute(t.fn, name, value), substitute(t.arg, name, value))
    if isinstance(t, Abs):
        if t.param == name:
            return t                       # name এখানে shadowed, ভেতরে যাওয়ার দরকার নেই
        if t.param in free_vars(value):
            # capture হতে যাচ্ছে! আগে alpha-rename করো
            new_param = fresh(t.param)
            renamed_body = substitute(t.body, t.param, Var(new_param))
            return Abs(new_param, substitute(renamed_body, name, value))
        return Abs(t.param, substitute(t.body, name, value))


def beta_step(t):
    """একধাপ normal-order (বাইরের-প্রথমে) reduction। কিছু না বদলালে None।"""
    if isinstance(t, App):
        if isinstance(t.fn, Abs):                       # সরাসরি redex — এটাই আগে reduce করো
            return substitute(t.fn.body, t.fn.param, t.arg)
        reduced_fn = beta_step(t.fn)
        if reduced_fn is not None:
            return App(reduced_fn, t.arg)
        reduced_arg = beta_step(t.arg)
        if reduced_arg is not None:
            return App(t.fn, reduced_arg)
        return None
    if isinstance(t, Abs):
        reduced_body = beta_step(t.body)
        return Abs(t.param, reduced_body) if reduced_body is not None else None
    return None                                          # Var — আর reduce হয় না


def normalize(t, limit=100):
    for step in range(limit):
        nxt = beta_step(t)
        if nxt is None:
            return t, step                               # normal form পাওয়া গেছে
        t = nxt
    return t, limit                                       # limit ছুঁয়ে ফেলল — সম্ভবত loops


# ── TRUE a b → a  পরীক্ষা ──────────────────────────────────────
TRUE = Abs("x", Abs("y", Var("x")))
expr = App(App(TRUE, Var("a")), Var("b"))
result, steps = normalize(expr)
print(f"TRUE a b  ⟶*  {result}   ({steps} steps)")

# ── Variable capture পরীক্ষা: (λx. λy. x) y ────────────────────
capture_test = App(Abs("x", Abs("y", Var("x"))), Var("y"))
result2, steps2 = normalize(capture_test)
print(f"(λx.λy.x) y  ⟶*  {result2}   ({steps2} steps) — free 'y' capture হলো না")

# ── Ω = (λx.xx)(λx.xx) — কখনো থামে না ──────────────────────────
omega_body = Abs("x", App(Var("x"), Var("x")))
omega = App(omega_body, omega_body)
result3, steps3 = normalize(omega, limit=5)
print(f"Ω  ⟶*  {result3}   ({steps3} steps — limit-এ থামানো হলো, normal form নেই)")

প্রত্যাশিত আউটপুট:

TRUE a b  ⟶*  a   (2 steps)
(λx.λy.x) y  ⟶*  (\v0. y)   (1 steps) — free 'y' capture হলো না
Ω  ⟶*  ((\x. (x x)) (\x. (x x)))   (5 steps — limit-এ থামানো হলো, normal form নেই)

দ্বিতীয় ফলাফলে লক্ষ্য করুন — v0 একটা fresh variable name, আর y (আসল free variable) অক্ষত আছে। যদি substitute-এ alpha-rename করার শর্তটা (t.param in free_vars(value)) বাদ দিতেন, ফলাফল হতো ভুলভাবে (\y. y) — ঠিক যেমন lesson-এর মূল টেক্সটে variable capture বিভাগে হাতে দেখিয়েছিলাম।

তৃতীয় ফলাফলে Ω limit ছুঁয়ে থেমেছে, কখনো normal form-এ পৌঁছায়নি — ঠিক যেমন গাণিতিক বিশ্লেষণে দেখিয়েছি।

নিজে বাড়ান:

SUCC, PLUS-এর জন্য Abs/App/Var দিয়ে term বানান আর normalize চালান — to_int-এর মতো একটা helper লিখে ফলাফল পড়ুন
beta_step-কে বদলে applicative order (ভেতরের redex আগে) বানান, আর (λx. y) Ω test করুন — normal order-এ থামে, applicative order-এ কী হয়?
Y combinator বানিয়ে একটা non-recursive g-এর সাথে Y g চালান (সতর্কতা: step limit ছোট রাখুন, Y-এর reduction দ্রুত deep হয়ে যায়)
একটা PAIR/FIRST/SECOND test যোগ করুন, normal form পর্যন্ত পুরো reduction trace print করে দেখুন

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

Lambda calculus যেখানে বাস্তবে বাস করে

Lisp — নামটাই বংশপরিচয় বলে দেয়। John McCarthy ১৯৫৮ সালে Lisp ডিজাইন করার সময় lambda calculus থেকে সরাসরি অনুপ্রাণিত হয়েছিলেন — lambda keyword সরাসরি Church-এর λ থেকে। প্রতিটা আধুনিক Lisp dialect (Scheme, Common Lisp, Clojure) এই উত্তরাধিকার বহন করে।

Haskell — সবচেয়ে বিশুদ্ধ বংশধর। Haskell-এ প্রতিটা ফাংশন curried (lambda calculus-এর মতোই একক-argument), আর ভাষার পুরো type system type-theory-and-curry-howard লেসনে আসা typed lambda calculus-এর সরাসরি সম্প্রসারণ। Haskell-এর \x -> x + 1 syntax লক্ষ্য করুন — \ টা আক্ষরিক অর্থে λ-এর ASCII-বান্ধব প্রতিস্থাপন।

Python-এর lambda keyword। সরাসরি, আক্ষরিক নাম-উত্তরাধিকার। lambda x: x + 1 সেই একই λx. x+1।

JavaScript-এর arrow function ও closure। x => x + 1 একই জিনিস, ভিন্ন syntax। আর programming-languages/closures-and-environments-এ যা “code pointer + captured environment” হিসেবে দেখেছিলেন, সেটা lambda calculus-এর free variable capture-এর সরাসরি runtime বাস্তবায়ন — PAIR-এর মতো Church encoding-এ আমরা এটাই হাতে-কলমে দেখেছি এই লেসনে।

Beta reduction ≈ inlining। compilers/optimizations-এর function inlining আক্ষরিকভাবেই beta reduction — একটা function call-কে তার body দিয়ে replace করা, argument substitute করে। Compiler optimization-এর একটা বড় অংশ আসলে বিভিন্ন কৌশলে beta reduction প্রয়োগ করা।

SKI combinator calculus — variable-ই বাদ দিয়ে দেওয়া। যদি variable নামও সরিয়ে ফেলতে চান, S, K, I — মাত্র তিনটা combinator দিয়ে lambda calculus পুরোপুরি পুনর্নির্মাণ করা যায় (K = λx.λy.x — লক্ষ্য করুন, এটাই আমাদের TRUE!)। এই “point-free” style modern functional programming-এ (Haskell-এর ., flip-এর মতো combinator) এখনও দেখা যায়।

Proof assistant। পরের লেসনে আমরা দেখব কীভাবে (typed) lambda calculus সরাসরি গাণিতিক প্রমাণের ভাষা হয়ে যায় — Curry-Howard correspondence।

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

“Lambda calculus শুধু একটা নোটেশন — 'আসল' গণনা তো Turing machine-এ হয়, lambda calculus তার একটা সরলীকৃত বর্ণনা মাত্র।”

না — দুটোই সমান শক্তিশালী, স্বাধীন, সম্পূর্ণ মডেল, কোনোটা অন্যটার “বর্ণনা” না।

Church (lambda calculus) আর Turing (machine) সম্পূর্ণ আলাদাভাবে, প্রায় একই সময়ে (১৯৩৬), দুইটা ভিন্ন প্রশ্নের সমাধান করতে গিয়ে দুইটা মডেল আবিষ্কার করেন — Church decidability সমস্যা থেকে, Turing “effectively calculable”-এর একটা mechanical সংজ্ঞা থেকে। পরে Turing নিজেই প্রমাণ করেন দুইটা মডেল equivalent power — যেকোনো lambda-computable function Turing-computable, আর উল্টোটাও। এটাই Church-Turing thesis-এর ভিত্তি।

lambda calculus কোনোভাবেই “সরলীকরণ” না — বরং এটা একটা সম্পূর্ণ ভিন্ন foundational ভাষা, যা থেকে functional programming-এর পুরো পরিবার এসেছে, ঠিক যেমন Turing machine থেকে imperative/machine-model programming-এর পরিবার এসেছে।

“Church numeral হলো computer-এ সংখ্যার আসল representation।”

না — বাস্তব কম্পিউটার binary two’s complement বা IEEE-754 ব্যবহার করে (computer-representation module), Church numeral না।

Church numeral একটা তাত্ত্বিক/foundational কৌশল — দেখানোর জন্য যে lambda calculus-এর কোনো built-in সংখ্যা primitive লাগে না, তবু সংখ্যা এনকোড করা সম্ভব। ব্যবহারিকভাবে এটা ভয়ানক অদক্ষ — n-এর উপর যেকোনো operation O(n) function application লাগে, যেখানে hardware integer arithmetic constant-time। Experiment section-এর MULT(2)(3) উদাহরণেই এই অদক্ষতা দেখা গেছে।

Church encoding-এর মূল্য conceptual: এটা প্রমাণ করে computation-এর জন্য “primitive data type” আসলে অপরিহার্য না — একটা যথেষ্ট শক্তিশালী function-composition ব্যবস্থা থেকেই সবকিছু derive করা যায়।

“Beta reduction order কোনো ব্যাপার না — যে কোনো ক্রমে reduce করলে একই ফলাফল আসবে।”

চূড়ান্ত ফলাফল (যদি কোনো normal form থাকে) একই — এটাকে বলে Church-Rosser theorem (confluence)। কিন্তু প্রতিটা reduction strategy সেই normal form-এ পৌঁছায় না।

Lesson-এর মূল টেক্সটের (λx. y) Ω উদাহরণ ঠিক এটাই দেখায় — applicative order (আগে argument reduce করা, call-by-value-এর মতো) Ω-তে চিরকাল আটকে থাকে, normal order (আগে বাইরের redex, call-by-name-এর মতো) সরাসরি y-তে পৌঁছায়।

এটা তাত্ত্বিক কৌতূহল না — সরাসরি ভাষা-ডিজাইনের সিদ্ধান্ত। programming-languages/evaluation-strategies-এ eager (Python, JavaScript) বনাম lazy (Haskell) evaluation-এর behavioral পার্থক্য — যেমন একটা infinite list তৈরি করে তার শুধু প্রথম উপাদান ব্যবহার করা Haskell-এ কাজ করে কিন্তু eager ভাষায় infinite loop — এই একই normal-order বনাম applicative-order পার্থক্যের প্রত্যক্ষ প্রতিফলন।

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

হাতে ধাপে ধাপে reduce করুন normal form পর্যন্ত:

(λx. λy. y x) (λz. z) a

প্রয়োগ

Application বাম-সংযোজী: এটা ((λx. λy. y x) (λz. z)) a।

ধাপ ১ — বাইরের redex: (λx. λy. y x)-কে (λz.z)-এর উপর প্রয়োগ, x-কে (λz.z) দিয়ে replace:

$\longrightarrow\ (\lambda y.\, y\ (\lambda z.\,z))\ a$

ধাপ ২ — এখন (λy. y (λz.z))-কে a-এর উপর প্রয়োগ, y-কে a দিয়ে replace:

$\longrightarrow\ a\ (\lambda z.\, z)$

এখানে আর কোনো redex নেই — a একটা free variable (ফাংশন নয়, তাই আরও প্রয়োগ করা যায় না)। Normal form: a (λz. z) — “a-কে identity function-এর উপর প্রয়োগ করা” — যদি a নিজে একটা ফাংশন হয়, তবেই এটা আরও reduce হবে, কিন্তু এখানে a একটা free variable, তাই এখানেই থামে।

এই term-টায় free ও bound variable আলাদা করুন, তারপর বলুন কেন λx. (λy. y x) x-কে y-এর জায়গায় x বসিয়ে সরল করার চেষ্টা করলে capture ঘটবে — capture এড়াতে alpha conversion কীভাবে প্রয়োগ করবেন?

λx. (λy. y x) x

যুক্তি

Free/bound বিশ্লেষণ: পুরো term-টা λx. দিয়ে বাঁধা, তাই এর ভেতরের কোনো x-ই free না — পুরো term বন্ধ (closed), কোনো free variable নেই। ভেতরের λy. y x-এ y bound (নিজের λy-এর সাথে), x — এই sub-expression-এর দৃষ্টিতে — free (কারণ λy x-কে বাঁধে না), যদিও পুরো term-এর দৃষ্টিতে এটা বাইরের λx-এর সাথে bound।

Capture কোথায় ঘটতে পারত: যদি আমরা (λy. y x)-কে সরাসরি আলাদাভাবে reduce করতে চাইতাম, ধরুন এটাকে x-এর জায়গায় নিজেই কিছু বসানোর (self-application-এর মতো পরিস্থিতি) দরকার হতো, আর যদি সেই নতুন মানের মধ্যে একটা free y থাকত, তাহলে (λy. y x)-এর ভেতরের bound y সেই free y-কে গিলে ফেলত। এই নির্দিষ্ট term-এ সরাসরি এমন redex এখনই নেই ((λx. ...) x-এর মতো কোনো বাইরের abstraction প্রয়োগ হচ্ছে না, পুরো জিনিসটা ইতিমধ্যে normal form-এর কাছাকাছি — λx. এর ভেতরে (λy. y x) x একটা redex, y-কে x দিয়ে replace করলে x x পাওয়া যায়, কোনো capture হয় না এক্ষেত্রে কারণ substitute হওয়া মান x নিজে λy-এর bound variable-এর সাথে সংঘর্ষে যায় না)।

সাধারণ নিয়ম হিসেবে: যখনই (λp. body) কে কোনো মান v -এর উপর প্রয়োগ করা হয় এবং body-এর ভেতরে এমন কোনো λq. ... sub-abstraction থাকে যেখানে q, v-এর কোনো free variable-এর সাথে নাম-সংঘর্ষ করে, তখনই capture-এর ঝুঁকি। প্রতিরক্ষা: substitution-এর আগে সেই অভ্যন্তরীণ q-কে একটা fresh নাম দিয়ে alpha-rename করে নেওয়া (build section-এর substitute function-এ ঠিক এই চেকটাই t.param in free_vars(value) লাইনে করা হয়েছে)।

মূল শিক্ষা: capture এড়ানোর নিয়মটা mechanical এবং সবসময় প্রযোজ্য — substitute করার আগে সবসময় চেক করুন, প্রতিস্থাপিত হতে যাওয়া মানের কোনো free variable, target abstraction-এর bound variable-এর সাথে সংঘর্ষ করছে কি না।

SUCC = λn. λf. λx. f (n f x) ব্যবহার করে দেখান SUCC 1 reduce করলে Church numeral 2 (λf. λx. f (f x)) পাওয়া যায়।

প্রয়োগ

1 = λf. λx. f x।

\begin{aligned} \text{SUCC}\ 1 &= (\lambda n.\lambda f.\lambda x.\, f\,(n\,f\,x))\ (\lambda f.\lambda x.\, f\,x) \\ &\longrightarrow \lambda f.\lambda x.\, f\,\big((\lambda f.\lambda x.\,f\,x)\ f\ x\big) \qquad [n \text{-কে replace}] \end{aligned}

এখন ভেতরের (λf.λx. f x) f x অংশটা আলাদাভাবে reduce করি (variable নাম-সংঘর্ষ এড়াতে ভেতরের bound f,x-কে সাময়িকভাবে f',x' ধরে নিচ্ছি — আসল substitution-এ alpha-rename প্রযোজ্য হবে):

$(\lambda f'.\lambda x'.\, f'\,x')\ f\ x \ \longrightarrow\ (\lambda x'.\, f\,x')\ x \ \longrightarrow\ f\,x$

তাহলে সম্পূর্ণ ফল:

$\lambda f.\lambda x.\, f\,(f\,x)$

এটাই ঠিক Church numeral 2-এর সংজ্ঞা। ✓ প্যাটার্নটা স্পষ্ট: SUCC শুধু n-এর ভেতরের f-প্রয়োগের চেইনে আরেকটা f যোগ করে দেয় — ঠিক যেমন mathematics/induction-এ inductive step “একটা বেশি” যোগ করে base case থেকে পরের case-এ যায়।

Ω = (λx. x x) (λx. x x)-এর কোনো normal form নেই। এই সত্যটা cs-theory-র halting problem-এর সাথে কীভাবে যুক্ত? (শুধু “উভয়টাই থামে না” বলাটা যথেষ্ট উত্তর না — সম্পর্কটা ব্যাখ্যা করুন।)

যুক্তি

সম্পর্কটা কাকতালীয় মিল না — এটা একটা গভীরতর কাঠামোগত সমতা থেকে আসে।

Lambda calculus Turing-সমতুল্য (Church-Turing thesis)। এর মানে: “একটা lambda calculus term কি normal form-এ পৌঁছায়?” প্রশ্নটা আর “একটা Turing machine কি তার ইনপুটে থামে?” প্রশ্নটা — দুটোই একই কাজ করে এমন একটা encoding দিয়ে একে অপরে রূপান্তরযোগ্য। যদি একটা প্রশ্নের সমাধানকারী algorithm থাকত, অন্যটাও সমাধানযোগ্য হয়ে যেত।

cs-theory/turing-machines-এর পরবর্তী decidability লেসনগুলোতে প্রমাণিত হয় যে halting problem undecidable — কোনো general algorithm নেই যা যেকোনো Turing machine + input দেখে নির্ভুলভাবে বলতে পারে “থামবে” বা “থামবে না”। যেহেতু lambda calculus সমশক্তির, “একটা lambda term normal form-এ পৌঁছায় কি না” প্রশ্নটাও undecidable — এটাকে বলা হয় “normalization problem”।

Ω তাই একটা নির্দিষ্ট, প্রমাণযোগ্য উদাহরণ (হাতে reduce করে সরাসরি দেখানো যায় এটা চিরকাল লুপ করে), কিন্তু এটা প্রমাণ করে না undecidability নিজে — undecidability মানে “কোনো general algorithm সব term-এর জন্য সঠিক উত্তর দিতে পারবে না”, Ω শুধু একটা concrete term যেটার জন্য উত্তরটা “না, থামে না” এবং সেটা আমরা হাতে verify করতে পারি। সাধারণ, arbitrary term-এর জন্য এই প্রশ্নের উত্তর mechanical ভাবে বের করার কোনো universal পদ্ধতি নেই — এটাই মূল দাবি, যা সরাসরি halting problem-এর undecidability থেকে আসে (দুই দিকেই reduction করা যায়)।

Church boolean আর pair ব্যবহার করে একটা NOT ফাংশন এবং একটা ছোট “linked list” এনকোডিং (একটা NIL মান আর একটা CONS/ISNIL/HEAD/TAIL সেট) ডিজাইন করুন। আপনার ডিজাইন ব্যাখ্যা করুন — কেন এটা কাজ করবে।

ডিজাইন

NOT: একটা boolean নিয়ে বিপরীতটা ফেরত দিতে হবে। সহজ উপায় — IF b FALSE TRUE:

$\text{NOT} = \lambda b.\, b\ \text{FALSE}\ \text{TRUE}$

যাচাই: NOT TRUE = TRUE FALSE TRUE (যেহেতু b=TRUE মানে “প্রথমটা বাছো”) = FALSE ✓। NOT FALSE = FALSE FALSE TRUE (“দ্বিতীয়টা বাছো”) = TRUE ✓।

Linked list — NIL, CONS, ISNIL, HEAD, TAIL:

তালিকার মূল ধারণা: হয় এটা খালি (NIL), অথবা একটা head + বাকি tail (CONS h t)। Church pair-এর সাথে একটা “is this nil?” flag যোগ করে বানানো যায়:

$\text{NIL} = \text{PAIR}\ \text{TRUE}\ \text{TRUE} \qquad \text{(দ্বিতীয় উপাদানটা এখানে অপ্রাসঙ্গিক, placeholder)}$

$\text{CONS} = \lambda h.\, \lambda t.\, \text{PAIR}\ \text{FALSE}\ (\text{PAIR}\ h\ t)$

$\text{ISNIL} = \lambda \ell.\, \text{FIRST}\ \ell$

$\text{HEAD} = \lambda \ell.\, \text{FIRST}\ (\text{SECOND}\ \ell) \qquad \text{TAIL} = \lambda \ell.\, \text{SECOND}\ (\text{SECOND}\ \ell)$

কেন এটা কাজ করে — ডিজাইনের যুক্তি:

প্রতিটা লিস্ট-value একটা pair, যার প্রথম slot-টা একটা tag — TRUE মানে “আমি nil”, FALSE মানে “আমি একটা cons cell”। ISNIL শুধু সেই tag বের করে ফেরত দেয় — সরাসরি Church boolean, যা IF-এর সাথে সরাসরি ব্যবহারযোগ্য।

CONS h t দ্বিতীয় slot-এ আরেকটা pair রাখে (h, t) — তাই HEAD আর TAIL দুই ধাপে pair unwrap করে: প্রথমে বাইরের pair-এর দ্বিতীয় slot (SECOND ℓ, যা (h,t) pair দেয়), তারপর তার প্রথম বা দ্বিতীয় slot (FIRST/SECOND) দিয়ে h বা t বের করে।

NIL-এর দ্বিতীয় slot-এ কী আছে সেটা কখনো পড়া হবে না (কারণ ভালো ডিজাইনে সবসময় ISNIL আগে চেক করা হয়), তাই placeholder হিসেবে যেকোনো মান বসানো যায় — এখানে TRUE বেছে নেওয়া হয়েছে শুধু সরলতার জন্য।

এই একই প্যাটার্ন — “tag + payload pair” — বাস্তব ভাষায় algebraic data type/tagged union বাস্তবায়নের সরাসরি পূর্বসূরি, যা type-theory-and-curry-howard-এ sum type হিসেবে আরও formally আসবে।

এরপর কী

আমরা দেখলাম untyped lambda calculus-এ সব চলে — এমনকি Ω-এর মতো চিরকাল-লুপ-করা term-ও ব্যাকরণগতভাবে সম্পূর্ণ বৈধ। এই স্বাধীনতাই এর শক্তির উৎস, কিন্তু এটাই একটা সমস্যাও — “এই program কি আদৌ থামবে” সেই প্রশ্নের কোনো mechanical উত্তর নেই।

পরের লেসনে আমরা lambda calculus-এ type যোগ করব — প্রতিটা term-এর উপর একটা শৃঙ্খলা চাপিয়ে দেব যা Ω-এর মতো term-কে ব্যাকরণগতভাবেই বাতিল করে দেয়। আর সেই path ধরেই পৌঁছাব ২০ শতকের সবচেয়ে চমকপ্রদ গাণিতিক পর্যবেক্ষণগুলোর একটায়: একটা প্রমাণ আর একটা প্রোগ্রাম — এই দুটো জিনিস আসলে একই জিনিস। এটাই Curry-Howard correspondence।

Lambda Calculus — তিনটা নিয়মে সব গণনা

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

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

আগে এটা বুঝি

মূল ধারণা

Syntax — তিনটা নিয়মে একটা ব্যাকরণ

Abstraction — নামহীন ফাংশন

Application — প্রয়োগ

Currying — সব ফাংশন এক-argument

Parenthesization convention

মূল ধারণা

Beta reduction — একমাত্র computation rule

উদাহরণ ১ — সরাসরি

উদাহরণ ২ — দুই ধাপ, currying-সহ

Redex, normal form, আর non-termination

মূল ধারণা

Free ও bound variable, আর alpha conversion

Variable capture — যেখানে naive substitution ভেঙে পড়ে

ভেতরে কী ঘটছে

Church Encoding — শুধু ফাংশন দিয়ে ডেটা বানানো

Boolean

Pair

উদাহরণ

Church numeral — সংখ্যাও শুধু function

Successor — এক যোগ করা

Addition

Recursion ছাড়া recursion — Y combinator

নিজে চালিয়ে দেখুন

Python-এ lambda calculus চালানো — Church encoding সত্যিই কাজ করে দেখা

নিজে বানান

একটা মিনিয়েচার beta-reducer লেখা

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

Lambda calculus যেখানে বাস্তবে বাস করে

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

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

এরপর কী

আরও পড়ুন

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

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

◔আগে এটা বুঝিWhy this matters

◆মূল ধারণাCore concept

Syntax — তিনটা নিয়মে একটা ব্যাকরণ

Abstraction — নামহীন ফাংশন

Application — প্রয়োগ

Currying — সব ফাংশন এক-argument

Parenthesization convention

◆মূল ধারণাCore concept

Beta reduction — একমাত্র computation rule

উদাহরণ ১ — সরাসরি

উদাহরণ ২ — দুই ধাপ, currying-সহ

Redex, normal form, আর non-termination

◆মূল ধারণাCore concept

Free ও bound variable, আর alpha conversion

Variable capture — যেখানে naive substitution ভেঙে পড়ে

⚙ভেতরে কী ঘটছেUnder the hood

Church Encoding — শুধু ফাংশন দিয়ে ডেটা বানানো

Boolean

Pair

▶উদাহরণExample

Church numeral — সংখ্যাও শুধু function

Successor — এক যোগ করা

Addition

Recursion ছাড়া recursion — Y combinator

⌘নিজে চালিয়ে দেখুনExperiment

Python-এ lambda calculus চালানো — Church encoding সত্যিই কাজ করে দেখা

⚒নিজে বানানBuild it yourself

একটা মিনিয়েচার beta-reducer লেখা

◉বাস্তব সিস্টেমেReal-world usage

Lambda calculus যেখানে বাস্তবে বাস করে

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

?বুঝেছেন কি না দেখুনCheck understanding

→এরপর কীNext step

আরও পড়ুন

আগে এটা বুঝি

মূল ধারণা

মূল ধারণা

মূল ধারণা

ভেতরে কী ঘটছে

উদাহরণ

নিজে চালিয়ে দেখুন

নিজে বানান

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

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

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

এরপর কী