# 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.

510 questions
Filter by
Sorted by
Tagged with
15 views

### λ-calculus: When is it possible to split a term into two or more expressions, so that each can be used in separate β-reductions?

In the $\lambda$-calculus expression: $$(\lambda x.\lambda y.xy)(f(f(a)))$$ Can the subexpression $(f(f(a))$ be split into two terms, $M$ and $N$? (Maybe, via $\alpha$-conversion?) If so, what could ...
45 views

### How to read/verbalize lambda expressions? What is (λx.λy).M?

In lambda calculus, application is left associative. That is, if M, N, and P are expressions,...
35 views

### Minimum number of distinct variables needed for lambda calculus to be Turing-complete?

Suppose you start with your everyday vanilla untyped lambda calculus, but restrict the alphabet to a finite number of variables. What is the minimum number of variables you need for Turing-...
46 views

### Untyped λ-calculus: proof that for any binary relation $R \vDash \lozenge \Rightarrow R^* \vDash \lozenge$

I'm currently in the process of reading Barendregt's "The Lambda Calculus - Its Syntax and Semantics" (1985 revised edition) and I've stumbled across a lemma whose proof I can't quite ...
46 views

### Structure of proof by induction in lambda calculus

I want to prove some theorems in lambda calculus using induction on the length of the term. Surprisingly, I haven't been able to find a single simple and complete proof online that uses this approach. ...
97 views

### Sequencing function applications in beta reduction

I am working problems in Hindley and Seldin. The 𝛽-reduction for this formula eludes me at a certain step, because I am having trouble understanding the ordering of function application. Yes, the ...
33 views

### Lambda notation for abstraction (Set theory).

I'm trying to solve a problem in Suppes' "Axiomatic set theory". It's about functions and lambda notation for abstraction, in the framework of ZFS set theory. I've defined, as usual, ...
73 views

### Is there a set-based semantics for the untyped lambda calculus?

Is there a set-based semantics for the untyped lambda calculus? As an example, here's a simple set-based semantics for the simply typed lambda calculus (henceforth STLC). It is extremely naive and ...
98 views

### How exactly is lambda calculus the foundation for functional programming languages?

One of the question on usability of lambda calculus highlighted that lambda calculus is the foundation for programming languages, including Haskell and Lisp. How is that exactly? Do compilers in ...
89 views

### Where and how lambda calculus is used?

So, I have been learning about lambda calculus at university and it seems too abstract and theoretical for me. Is lambda calculus used anywhere practically? P.S. I tried searching Haskell compiler ...
77 views

40 views

### Lambda calculus list encodings [duplicate]

I'm working on a following problem using lists in labda calculus. Now, I wanna show that the following term β -reduces to 6 : [3, 2, 1] times 1 Numerals 1 , 2 , 3 , ...
47 views

### Boolean function encoded with lambda calculus

I have a function $G = \lambda xy.(M(N x y))$, where $M = \lambda zxy.zyx$ and $N = \lambda xy.xyx$, which encodes a boolean function of two arguments $f(x,y)$ By $\beta$-reduction, $G T T$ and $G T F$...
36 views

### Beta reducing $SS(SK)$ using SKI calculus

I have an expression to $\beta$-reduce and I managed to brute force it using the $\lambda$-calculus. I was wondering though, if I could make it in less steps, than what I did, using the $SKI$-calculus....
49 views

### Lambda representability for boolean function

I have the following $\lambda$-term $$F=\lambda xy.(M(Nxy))$$ where $$M=\lambda zxy.zyx \qquad N=\lambda xy.xxy$$ The term $F$ represents some boolean function of two arguments $f(x,y)$. So I need to ...
27 views

### Is the untyped lambda calculus consistent if equations containing non-β-normal forms are void?

Consider the function $f = \lambda x \mapsto \neg (x\ x)$ where $\neg$ is negation. It then follows that $$f\ f = \neg (f\ f)$$ Thus proving a contradiction, but $(f\ f)$ is an expression that does ...
42 views

### Doesn't lambda K-calculus include lambda I-calculus?

To mock a mockingbird, chapter 18: From just S and K you can derive any combinatorial bird whatsoever! Same book, chapter 19 […] with just the two birds J and I, we would ultimately get the same ...
63 views

### How are TRUE/FALSE booleans acceptable in lambda calculus? [duplicate]

I'm working my way through an introduction to lambda calculus, and it seems to start from the premise that TRUE and FALSE (as ...
34 views

### How would this lambda function reduce?

Let's say I have TRUE and FALSE defined as follows: $$\pmb{T} = \lambda ab.a$$ $$\pmb{F} = \lambda ab.b$$ Now I can define a <...
49 views

### Understanding a basic premise in lambda calculus

From the following lamba calculus text it mentions: To motivate the $\lambda$-notation, consider the everyday mathetmatical expression '$x-y$'. This can be thought of as defining either a function $f$...
56 views

### What to Substitute in a Lambda Calculus?

I am confused firstly about how to differentiate between a bound variable and a free variable, so if someone could explain that with an example, that would be great. Once I know the difference while ...
35 views

### Product type in Type theory

I am new to type theory. It was explained that $\Pi$-type is like cartesian product of types. Firstly, in set theoretic formalization of mathematics, a function $f$ from $\mathbb{N}$ to $\mathbb{R}$ ...
72 views

This is some kind of weird notation. I know how $\;\hat{a}\;$ was used in the Principia Mathematica (as an equivalent of $\;\eta$-reduction in lambda calculus), but what does it do here $\;\hat{a}(a=a.... 1answer 71 views ###$\lambda$-calculus: find$F$such that$FI = x$and$FK = y$I'm learning some$\lambda$-calculus using the following book: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf I'm having some trouble with exercise 2.12 (iii) on page 15. ... 0answers 10 views ### Given G =$ \lambda A \in P(Y). f^{-1}[A] $. For any$ f \in X \rightarrow Y $show:$ G $is Injective$\iff  f $is onto$ Y $. Problem: We define the function$ G = \lambda A \in P(Y). f^{-1}[A] $, Prove that for every$ X , Y $and$ f \in X \rightarrow Y $:$ G $is Injective$\iff  f $is onto$ Y $. Clarifications: ... 1answer 45 views ### Why is reflexivity a feature of multi-step β-reduction, and not of β-reduction? I understand the need to distinguish between two algorithms, even when one is enclosed in another. Transitivity as a feature of multi-step reduction makes perfect sense, since we literally need ... 2answers 65 views ### Differences in book definitions of$\beta$-reduction leading to confusion on when an abstraction needs to be$\alpha$-converted I've been learning Lambda Calculus in my free time recently to try and learn how to make programming languages & interpreters. I am struggling a little bit with some inconsistencies on different ... 1answer 45 views ### Question about de Bruĳn Notation of lambda calculus https://www.cs.cornell.edu/courses/cs4110/2016fa/lectures/lecture15.pdf One way to avoid the tricky interaction between free and bound names in the substitution operator is to pick a representation ... 0answers 109 views ### Defining xor using lambda calculus True and False in lambda calculus are defined like$ T = λxy.x$and$ F = λxy.y$how to define xor that computes the exclusive or of two boolean values ? 1answer 35 views ### Evaluating lambda expression call by value Beta reduction$ + = λmnab.m a((n a) b)$I have to show that$2 + 3 \triangleright_\beta $5 what I understand from the lambda expression of + is that it takes 4 arguments m, n , a , b But when I have to ... 1answer 35 views ### Lambda Calculus Question: If for some λ-terms M and N we have Mx =β Nx. Does it necessarily imply that M =β N? I have a homework question that I can't figure out. Hope someone can help. Assume that for some$\lambda$-terms$M$and$N$we have$Mx =_\beta Nx$. Does it necessarily imply that$M =_\beta N$? Here ... 2answers 156 views ### Motivation behind Lambda Calculus? The lambda calculus provides a formalism broad used in theoreretical cs to write functions without giving them explicit names, it declares anonymous functions. That is at first glance it's just an ... 0answers 45 views ### Is$C$a cartesian closed category here? Let$C$be a category with, for each$X \in \text{Obj}(C)$, a comonad$F(X) : C \rightarrow C$and a monad$G(X) : C \rightarrow C$, such that$F(X) \vdash G(X)$, i.e. there is for each$X, Y, Z$, an ... 1answer 85 views ### (How) does lambda calculus encode/use associativity of function composition? I'm just learning about Lambda Calculus, so apologies if this is an obvious question, but given how useful and fundamental the associativity property of function composition is, (how) is this ... 3answers 1k views ### Function "evaluation" just means "composition"? I am self-studying and have a basic or naive question that follows from a simple observation. I have also included tags for type theory, etc because "evaluation" probably has a different ... 1answer 112 views ### SKI Calculus prefix notation of odd/even number I'm working on a homework with SKI calculus. I saw the hints in this very useful post. We basically defined SKI functions as: ... 1answer 61 views ### Parenthesization in Lambda Calculus I am trying to understand how parenthesization works in$λ$- calculus. All of the resources state the following : Applications are left associative Abstractions are right associative and extend as ... 1answer 41 views ### Beta Reduction Constraints The definition of$β$reduction is the following : $$(λx.M)N \rightarrow_{β} Μ[x∶=N]$$ So basically we stop treating$x$as a bound variable and we perform substitution of the now free variable$x$... 0answers 52 views ### Functions which are provably total in second order peano arithmetic Girard has a representation theorem claiming: The functions representable in$F$are exactly those which are provably total in second-order peano arithmetic$PA_2$. I believe the usual way to prove ... 1answer 72 views ### Beta Reduction in Lambda Calculus I came across the definition of beta reduction in Lambda Calculus which is : $$(λx.M)N \rightarrow_β Μ[\space x:= N \space]$$ under the constraint that the$FV(N)$are still free after the ... 1answer 37 views ### Substitution constraints in Lambda Calculus I came across this definition of Substitution in Lambda Calculus and I am trying to wrap my head around it.$$(λy.P)[x:=N] \equiv λy.(P\space[x:=N])$$ given two constraints :$y \notin FV(N)\space$or ... 1answer 72 views ### Interpretation of a term in Lambda Calculus Just started studying$λ$-calculus and I came across this$λ$-term : $$λx.λy.xy$$ As far as I understand this can be read as : Apply$x$to$y$The result of$(1)$is probably an expression say$E_1$... 1answer 62 views ### Lambda Calculus Terms According to what I've read so far a lambda calculus term is described as :$\langle term \rangle ::==\langle var \rangle |\space (\langle term \rangle\space \langle term \rangle) \space |\space (...
I'm slightly confused by the successor function for Church numerals. Written down in my textbook it is defined as follows: $$succ = \lambda n. \lambda f. \lambda x. n \;f \; (f \; x)$$ Therefore ...
In the $\lambda$-calculus, is the family of $\lambda$-terms $(N_i)_{i \in \mathbb{N}}$, defined below, a representation of Church numerals? I think it is, but how do I (sufficiently) show it? If not, ...