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.

Filter by
Sorted by
Tagged with
0
votes
1answer
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 ...
0
votes
1answer
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,...
1
vote
1answer
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-...
4
votes
1answer
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 ...
1
vote
1answer
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. ...
2
votes
2answers
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 ...
-1
votes
0answers
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, ...
6
votes
0answers
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 ...
3
votes
1answer
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 ...
1
vote
1answer
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 ...
3
votes
1answer
77 views

Proving terms using induction in LC

Expanding on the following question here and on the book on the $\lambda$-calculus I'm reading, I'm trying to prove the correctness of the given solution in a more complicated manner. Let $(F_n')_{n \...
2
votes
1answer
109 views

Lambda calculus - church encoding and lists

I'm reading a book on the $\lambda$-calculus and I'm stuck on a list of representations. While practising different lambda calculus tasks I've stumbled upon an interesting issue. Given two terms I ...
2
votes
1answer
51 views

Is this a valid reduction?

Someone told me this is a valid transformation, in the context of a full $\beta$-reduction. $$ \lambda f o o . f o o \rightarrow foo \label{1}\tag{1} $$ They seem pretty confident, and while it's ...
0
votes
0answers
28 views

XOR operation using lamba calculus and pré-operation

I recently posted a question with a similar title, but reading the community guidelines, I decided to improve it :) We can define the $AND$, $OR$ and $NOT$ operations in terms of the $T$ and $F$ ...
2
votes
1answer
203 views

Typed vs untyped lambda calculus in methods for haskell

Expanding a bit on the following questions and their answers: Give Lambda Calculus Term for Haskell Function Infinite lists in Lambda calculus.... I really like the answers to the two questions, but ...
3
votes
1answer
200 views

Lambda calculus defining terms according to description

I'm working on a problem I stumbled across online. The goal is to define terms for two use cases which are defined as follows: lists are encoded as: $ [N_1,N_2,...,N_k] ≜ λc.λn.c N_1 (c N_2 (...(c N_k ...
0
votes
0answers
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 , ...
4
votes
1answer
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$...
1
vote
1answer
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....
1
vote
1answer
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 ...
1
vote
0answers
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 ...
1
vote
1answer
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 ...
0
votes
0answers
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 ...
0
votes
0answers
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 <...
1
vote
2answers
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$...
3
votes
1answer
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 ...
1
vote
1answer
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}$ ...
0
votes
1answer
72 views

What does Quine mean by $\;\hat{a}\phi=\;$V?

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....
5
votes
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. ...
0
votes
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: ...
3
votes
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 ...
2
votes
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 ...
-2
votes
1answer
45 views

Question about de Bruijn 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 ...
0
votes
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 ?
0
votes
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 ...
3
votes
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 ...
2
votes
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 ...
3
votes
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 ...
0
votes
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 ...
25
votes
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 ...
3
votes
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: ...
2
votes
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 ...
2
votes
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$ ...
2
votes
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 ...
2
votes
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 ...
1
vote
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 ...
2
votes
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$ ...
2
votes
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 (...
1
vote
0answers
51 views

Lambda Calculus Church Encoding Successor Function

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 ...
3
votes
1answer
143 views

Representation of Church numerals

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

1
2 3 4 5
11