# Questions tagged [lambda-calculus]

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

489 questions
Filter by
Sorted by
Tagged with
95 views

### How, if possible, can we efficiently compute with lazy data structures in 𝜆-calculus?

In Haskell, we can use the following code to define fibonacci numbers, fibs = 1 : 1 : zipWith (+) fibs (tail fibs) And its time complexity is linear. I cannot find ...
31 views

### Equivalence between $\lambda$-calculus and recursive functions

I have two related questions: Do you know of any good reference to the recursive function / lambda-calculus equivalence in terms of computability, including proofs? Do you know of any reference to ...
44 views

### Lemma relating variable substitution to de Bruijn substitution

Notation: Let $t$ and $u$ be terms in the $\lambda$-calculus, and $x$ be a variable name. Let $[x\mapsto u]t$ be the substitution in $t$ of free variable $x$ for the term $u$. Specifically, I'm ...
35 views

### What are the fixed-points of the Y combinator?

Since the Y combinator itself is a function (albeit a higher-order one), I was wondering what the fixed-points of Y itself are.
29 views

### How to verify/proof that my lambda calculus is correct?

I was reading about proof assistants, formal verification etc, also I have a lambda calculus implementation. My question is: Is it possible to prove that my implementation is correct? In fact I have ...
28 views

### Lambda Calculus: Re-Ordering Arguments

Given any multivariable expression in Lambda Calculus (LC), e.g. for an arbitrary LC expression "op" for some non-commutative operation: ...
40 views

### Delayed "let" in SICP

In section 3.5.4 , i saw this block: ...
255 views

### What benefits are obtained by allowing the occurrence of free variables and open terms in lambda calculus?

Because of the existence of free variables in lambda calculus, the evaluation of open terms (at least as outlined here) is more complicated relative to the evaluation of closed terms since the ...
57 views

### Proving intuitionistic tautologies in Agda

I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law $$((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B$$ I ...
30 views

### On lambda calculus notation: FGa

If we've got this expression: FGa where F and G are functions (as well as a, of course; but let's treat a as a constant). It must be understood that: first apply F taking G as input; then apply the ...
55 views

### Can the Y-combinator really terminate?

My understanding of the Y-combinator is that it never terminates (Yg = g(Yg)). Its termination is only decided externally to the $\lambda$ specification when it has ...
117 views

### Is this definition of $\alpha$-equivalence correct?

I want to extend $\alpha$-equivalence to cover substitution. That is, I will implement runSubst_Term : Subst -> Tm -> Tm and prove: ...
29 views

### Is there a functional programming language with inherent change propagation?

Change propagation in programming environments is an add-on at the framework level such as React. There was a lot of work on dataflow virtual machines in the wake of Backus's Turing Award Lecture on ...
38 views

148 views

### Why should I care about lambda calculus

I am a programmer by hobby. I stumbled upon lambda calculus from Kevlin Henney's talk lambdas to the slaughter and I was sold! It was an interesting new way of thinking that's entirely different than ...
30 views

### How would you model Rust procedural macros?

In Rust programming language one can write a compiler extension function that works on abstract syntax tree, effectively modifying source code before it gets converted into machine instructions. In ...
184 views

### Normalization-by-evaluation for untyped lambda calculus which results in 𝛽𝜂-normal form

Usual NbE algorithms for untyped lambda calculus, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms. Is there algorithms to (efficiently) exploit ...
224 views

### Sequencing or continuation-passing in pure lambda-calculus

I am trying to solve the following exercise given here. Consider the following number representation. How to define the addition? ...
40 views

### Lambda calculus simplification excercise

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. (λx.λy.yx)z (λw.w) I am lost with this. if anyone could lead me in ...
128 views

### Is the term $(\lambda x.x)(y y)$ a normal form in call-by-value reduction strategy?

I am learning λ-calculus and I have some confusion about it. Is the term $(\lambda x.x)(y y)$ a normal form in call by value reduction strategy? (where $y$ is a free variable) From the wikipedia, it ...
117 views

### What's the internal language of the opposite of a Cartesian closed category?

I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories. What's the internal language of the opposite type of category? The rules dual to currying and ...
49 views

### How to write "∀x.F(x)" for "F(x)=λx.Φ(x)" in one expression (sequel from question about "∀(λφ. (φ x m→ φ y))"?

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context. So - I have anonymous Boolean-valued ...
146 views

### Can lists be defined in a special way so that they contain things of different type?

In https://www.seas.harvard.edu/courses/cs152/2019sp/lectures/lec18-monads.pdf it is written that A type $\tau$ list is the type of lists with elements of type $\tau$ Why must a list contain ...
Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term \$\lambda x_{\beta}. \;(x, \, ...