# Questions tagged [lambda-calculus]

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

265 questions
Filter by
Sorted by
Tagged with
466 views

2k views

351 views

### Reading list on rewriting systems?

I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
669 views

### Do Higher-Order Functions provide more power to Functional Programming?

My original question was: Is Kappa calculus less powerful than Lambda calculus? Does the lack of Higher-Order functions on a programming language excludes some programs that could only be written in ...
272 views

### Origin of Church encodings

In which paper did Alonzo Church first describe Church encoding? I can't find any articles that actually cite the paper, but I am interested in reading it.
193 views

### Labels for terms in the lambda calculus

In the lambda calculus, are there commonly accepted names for $x$ and $M$ when they appear in $\lambda x [M]$ ? Something along the lines of "binder" and "bindee"?
1k views

### Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
2k views

### What is the point of calling $\lambda$-calculus an algebra?

What is the difference of calling $\lambda$-calculus an algebra instead of a calculus? I raise this question because I read somewhere the line "$\lambda$-calculus is not a calculus but an algebra" (...
260 views

### Lambda Calculus - are these two expressions equivalent? [closed]

(λa.(λb.λc.b)) and (λa.λb.λc.b) I was wondering if someone could explain, using mostly English, what that lambda-calculus expression is supposed to mean, and whether there is any difference between ...
425 views

### Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

Normal Order Reduction (NOR) reduce the leftmost, outermost redex. Normal Order Evaluation (NOE) reduce the leftmost, outermost redex, but not within the body of abstractions. So (λw. (λx.x) z) is ...
3k views

### Functions that typed lambda calculus cannot compute

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi. As I am a beginner, some reiteration of background information ...
327 views

### How to define eta-equivalence for F-omega types?

There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus: via a plain relation $t_1 = t_2$, via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
1 vote
343 views

### Can "$x(\lambda y.P\;)z$" be $\beta$-reduced?

Consider the untyped $\lambda$-calculus expression $$x(\lambda y.P\;)z$$ ...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've ...