# Questions tagged [lambda-calculus]

For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

366 questions
31 views

### Syntactic proof that Peirce's law doesn't hold in simply-typed lambda calculus

This might have been asked before, but certainly I don't find any source. Even in the literature I've consulted, there is no such proof so far. Context In the context of the simply typed lambda ...
15 views

### Brackets in Lambda Calculus with multiple lambdas

How would you evaluate $\lambda x.\lambda x.\lambda x.x 1 2 3$? I cant figure out if the first lambda takes the 1 beta reduces, then the second lambda takes the 2 then beta reduces and finally the ...
32 views

79 views

### Why does Turing-computing (being an inconsistent formalism) has undecidable problems? [closed]

I'd like to apply Church-Turing thesis to Kleene-Rosser paradox: Since untyped lambda-calculus is an inconsistent formalism AND Turing machines are equal in decisive power to lambda-calculus SO We ...
81 views

### In Homotopy Type Theory, where does the lambda expression reside?

Background I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a ...
103 views

### What is the meaning of this Church numeral example?

There is an example of Church numeral, on the secion Encoding Datatypes of lambda calculus's wikipedia page. One way of ...
67 views

### Confused by the explanation of beta reduction of lambda calculus on wikipedia.

On this wikipedia article, there is an explanation of lambda calculus. In the section of Beta reduction, there is an Omega ...
46 views

### Transformations similar to Curry/Uncurry

The currying operator transforms a function of the form $(A\times B)\rightarrow C$ into an equivalent one of the form $A\rightarrow(B\rightarrow C)$. The uncurrying operator goes the other way round. ...
87 views

### Is it possible to express syntactic equality function in lambda calculus?

Let's denote truth and false by two suitable constants $T, F$ where $T \not=_\beta F$ where $\equiv$ is syntactic identity. Could I define a $\lambda$-term $E$ such that for $\lambda$-terms $X$ and ...
94 views