🔥 |
HOTNEW
β-reduction confluence proof — why does the Church-Rosser theorem actually hold?
by purrfect_β · I keep getting lost in the parallel reduction argument. Can someone walk through the strip lemma step by step? The diamond property is...
|
142replies |
9,882views |
lambda_neko »
2025-03-26 · 23:51
|
λ |
NEW
What exactly is η-reduction and when should I use it? Confused about extensionality
by eta_kitty · I understand β-reduction (substitution of argument for bound variable) but η-reduction (λx.f x → f when x∉FV(f)) feels mysterious to me...
|
37replies |
2,114views |
eta_kitty »
2025-03-26 · 21:18
|
🔥 |
HOT
SKI combinators — bracket abstraction algorithm, optimizations, and Turner's B, C, S', B', C' extensions
by S_combinator · Starting a comprehensive thread on translating λ-terms to combinators. The naive bracket abstraction produces exponential blowup so David Turner found...
|
203replies |
15,670views |
K_nyaan »
2025-03-25 · 17:40
|
λ |
SOLVED
Church numerals — proving predecessor takes O(n) β-steps, and is there a constant-time alternative?
by church_meow · The Rosser add definition (λn.λm.λz.λs. n (m z s) s) is constant-time, but the predecessor of Church numerals is infamously tricky. Compare Scott encoding...
|
58replies |
4,537views |
fixpoint_chan »
2025-03-24 · 09:22
|
λ |
Call-by-value vs. call-by-name vs. call-by-need — reduction strategies and their relationship to programming languages
by lazy_neko · CBN: outermost-leftmost first (Haskell lazy eval). CBV: innermost-leftmost (ML, Scheme). CBNeed: CBN with memoization. What are the formal operational semantics...
|
74replies |
5,891views |
Yuki_eta »
2025-03-23 · 18:05
|
🔥 |
HOTSOLVED
Scott encoding vs Church encoding — when does the pattern-matching approach win?
by Scott_catgirl · Scott encoding represents algebraic data types following their syntactic definition, unlike Church encoding which treats recursive types with right folds. Key difference:
|
117replies |
8,302views |
S_combinator »
2025-03-22 · 12:44
|
λ |
Fixed-point combinators zoo: Y, Z, Θ (Turing), and their differences under strict evaluation
by fixpoint_chan · The Y combinator (λf.(λx.f(xx))(λx.f(xx))) diverges under CBV. The Z combinator (λf.(λx.f(λv.xxv))(λx.f(λv.xxv))) is the CBV safe version. Turing's Θ = (λa.λb. b(aab))...
|
49replies |
3,719views |
purrfect_β »
2025-03-21 · 20:33
|
🔒 |
CLOSED
[DRAMA] Is untyped λ-calculus actually useful or should we just use System F? (heated debate)
by type_theory_tan · Thread locked after 300 posts. See pinned post for moderator summary. Both sides made good points. Untyped LC: universal computation, simplicity. System F: strong normalization...
|
300replies |
22,018views |
lambda_neko »
2025-03-19 · 03:15
|
λ |
The Lambda Cube — visualizing the 8 type systems from λ→ to the Calculus of Constructions (CoC)
by cube_meow · Barendregt's λ-cube has three axes: polymorphism (terms depending on types), type operators (types depending on types), dependent types (types depending on terms)...
|
91replies |
6,441views |
cube_meow »
2025-03-18 · 15:57
|
λ |
NEW
Alpha-equivalence and de Bruijn indices — implementing substitution without variable capture
by debruijn_chan · Variable capture in naïve substitution is the bane of every λ-calculus implementor. de Bruijn indices replace variables with natural numbers indicating binder depth...
|
33replies |
1,987views |
debruijn_chan »
2025-03-17 · 11:28
|
λ |
SOLVED
Church booleans — encoding if-then-else, and and or NOT in pure λ-calculus
by bool_nyan · TRUE := λt.λf.t, FALSE := λt.λf.f. The neat trick is that a Church boolean IS the if-then-else: b T F evaluates to T if b is TRUE, F otherwise. So AND := λb.λc. b c FALSE...
|
28replies |
3,203views |
church_meow »
2025-03-15 · 16:42
|
🔥 |
HOT
Optimal β-reduction and the BOHM implementation — sharing, graphs, and the Lévy-optimal strategy
by optimal_neko · Standard β-reduction can duplicate redexes unnecessarily. Lévy showed there's a notion of "optimal" reduction that shares work. The BOHM prototype outperformed...
|
156replies |
11,204views |
optimal_neko »
2025-03-14 · 08:19
|
λ |
Mogensen-Scott encoding of λ-terms as data — writing a self-interpreter in pure λ-calculus
by meta_meow · Mogensen extended Scott encoding so λ-terms can be represented as data objects inside λ-calculus itself. This enables metaprogramming and self-interpretation...
|
44replies |
2,875views |
S_combinator »
2025-03-12 · 21:00
|
λ |
SOLVED
Church pairs (λ-pairs) — encoding 2-tuples, n-tuples, and lists using pairing combinators
by pair_neko · PAIR := λx.λy.λf. f x y, FST := λp. p (λx.λy.x), SND := λp. p (λx.λy.y). We can extend to lists: nil = λc.λn.n, cons = λh.λt.λc.λn. c h (t c n) — that's Church list encoding!
|
22replies |
1,654views |
pair_neko »
2025-03-11 · 14:37
|
λ |
Parigot encoding — getting constant-time predecessor AND structural recursion at once
by parigot_chan · Church encoding: O(n) predecessor. Scott encoding: O(1) predecessor but you need Y for recursion. Parigot encoding: O(1) predecessor with built-in recursion. How?...
|
61replies |
4,020views |
fixpoint_chan »
2025-03-09 · 22:13
|
λ |
Normal forms: head normal form, weak head normal form, and beta normal form — definitions & differences
by NF_kitty · Not all λ-terms reduce to β-normal form (Ω = (λx.xx)(λx.xx) diverges). But understanding HNF and WHNF is crucial for implementing lazy evaluators...
|
39replies |
2,510views |
lazy_neko »
2025-03-07 · 10:55
|
λ |
SOLVED
Iota combinator — how does ι = λf.fSK make a Turing-complete language with one combinator?
by iota_nya · Iota defines ι := λx.xSK. Then S = ιι(ιι) and K = ι(ιι(ιι)) up to reduction. A universal combinator! Related to Jot and Lazy K languages...
|
31replies |
2,098views |
S_combinator »
2025-03-05 · 19:44
|
🔥 |
HOT
Curry-Howard isomorphism — propositions as types, proofs as programs (intuitionistic logic & λ→)
by proof_nyan · If types = propositions and terms = proofs, then function types = implication, product types = conjunction, sum types = disjunction, ⊥ = empty type. The correspondence goes...
|
188replies |
13,772views |
proof_nyan »
2025-03-03 · 07:31
|
λ |
Continuation-passing style (CPS) transform — defunctionalizing λ-terms for low-level compilation
by cps_catgirl · CPS transform makes control flow explicit. Every function takes an extra continuation argument. Useful for implementing exceptions, call/cc, and compiling to assembly...
|
55replies |
3,344views |
cps_catgirl »
2025-02-28 · 18:09
|
λ |
Denotational semantics of λ-calculus — Scott domains, continuous functions, and D∞ models
by domain_nya · Dana Scott showed in the 1970s that if only continuous functions are considered, a domain D with D≅[D→D] can be found, giving a model for untyped λ-calculus...
|
67replies |
4,891views |
domain_nya »
2025-02-25 · 13:20
|
λ |
Binary lambda calculus (BLC) — Tromp's minimalist universal λ-calculus with binary I/O encoding
by BLC_neko · Binary lambda calculus has one of the shortest Kolmogorov complexity universal machines. λ-terms are encoded in binary: 00 = λ, 01 = application, 1^n 0 = variable #n...
|
18replies |
1,102views |
BLC_neko »
2025-02-21 · 09:47
|
λ |
SOLVED
What is the SECD machine? Implementing a λ-calculus evaluator with Stack, Env, Control, Dump
by SECD_tan · Landin's SECD machine is a virtual machine for evaluating λ-calculus expressions. Stack holds intermediate results, Environment maps vars to values, Control is the...
|
42replies |
2,788views |
lazy_neko »
2025-02-17 · 22:02
|
λ |
η-expansion in practice — point-free style, optics, and when the compiler cares
by pointfree_nya · In Haskell you write f = map g instead of f xs = map g xs. That's η-reduction. But sometimes GHC needs the η-expanded form for optimisation. When and why?...
|
26replies |
1,873views |
eta_kitty »
2025-02-13 · 16:50
|