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.

24 questions
609 views

Meaning of variables and applications in lambda calculus

The wikipedia definition of lambda terms is: The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms: a variable, $x$, is ...
124 views

593 views

Fixed point combinator (Y) and fixed point equation

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states: In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can ...
941 views

Understanding η-conversion (Lambda Calculus)

Let $h \in A\rightarrow (B\rightarrow C)$ I'm trying to understand the following reduction: $$\lambda x\in A. \lambda y \in B.(h(x))(y) \\= \lambda x\in A.h(x) \\= h$$ Apparently, this is done by ...
308 views

I did not understand one thing in the proof of substitution lemma?

The substitution lemma in lambda-calculus is proved by the following way, but I just did not understand the application of induction hypothesis in it. The lemma as shown below, where $x$ and $y$ are ...
151 views

Actually defining functions in Church's simple type theory

I've been reading up on Church's simple type theory and much of the concepts make sense to me. However, I can't actually figure out how to define functions explicitly using the notation provided. ...
115 views

Lambda calculus: How to define a function that simulates $\neg p\vee q$?

I am making my first steps in lambda calculus, so please bear with me. I want to create a lambda function, that given two boolean expressions (either $F$ or $T$ - defined below), simulates the formula ...
149 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
836 views

$\lambda$-calculus: structural induction principle over $\Lambda$
The set $\Lambda$ is given inductively by: $x\in\Lambda$, if $x$ is a variable; $(\lambda x M)$, if $x$ is a variable and $M\in\Lambda$; $(MN)$, if both $M,N\in\Lambda$. Now, consider the structural ...