# Questions tagged [lambda-calculus]

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

460 questions
Filter by
Sorted by
Tagged with
20 views

I was reading http://barrywatson.se/lsi/lsi_delta_reduction.html, where ((+ 1) 2) →δ 3 is a δ-reduction. ((+ 1) ((+ 1) 1)) is a not a δ-redex. Wouldn't ((+ 1) ((... 1answer 25 views ### Beta reduction of S combinator in pure lambda calculus S is defined as S x y z = x z (y z) This suggest that (y z) should be evaluated just after ... 0answers 23 views ### What kind of automaton recognizes closed terms of the lambda calculus? There seems to be an interesting model of computation involved in determining whether a term from some programming language has any free variables. It's a tree traversal that seems almost like the ... 1answer 20 views ### Fixed Point Combinator Turing proof I have to proof that Turing's combinator is a fixed point operator, but I can't get it. I tried this: \begin{align*} Vg &= (UU)g = ((\lambda f.\lambda x.x(ffx)) (\lambda f.\lambda x.x(ffx)))g =... 1answer 73 views ### What is the diference between\lambda x.1$and$1$? I know that I can$(\lambda x.1) 0 \rhd_\beta 1$. This is the constant 1, but can I contract it automatically? I mean, is$1$the normal form of$(\lambda x.1)$? It seems reasonable to do it but when ... 1answer 42 views ### Is (λx.FV(A)) and (λx.FV(B)) β-equivalent? Does free variables have some meaning in lambda calculus? If I follow this β-reduction ... 0answers 21 views ### Other encodings of the natural numbers that are not the Church encoding or the Scott encoding Are there other encodings of the natural numbers in the untyped lambda calculus which are neither the Church encoding nor the Scott encoding? 0answers 19 views ### Imposing sortal restrictions on functions in the untyped lambda calculus In the simply typed lambda calculus if we have an addition operator,$+ : n \to n \to n$, its typing imposes that we can only combine it with something of a given type. So if$n$is the type of ... 1answer 78 views ### The difference between$\beta$-reduction and$let$These are the reduction rules associated with$\beta$reduction and$let$: $$(\lambda x. e_2) e_1 \to_{\beta} e_2 [e_1 / x]$$ $$let \,x = e_1 \textit{ in }e_2 \to e_2 [e_1/x]$$ These reduction rules ... 2answers 85 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 ... 1answer 20 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 ... 0answers 168 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 ... 2answers 202 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? ... 1answer 33 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 ... 0answers 43 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 ... 0answers 103 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 ... 0answers 47 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 ... 3answers 125 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 ... 1answer 305 views ### How to understand quantifier without predication “ ∀(λφ. (φ x m→ φ y))”? I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ... 1answer 101 views ### Creating a large tuple from smaller tuples via a monad or applicative 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, \, ...
89 views

The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).' Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
255 views

### The meaning and relevance of the locution ''no terminating implementation'' in type theory

In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that There is no terminating ...
26 views

### Constructing a monad via type synonyms of a particular kind

We can define a reader/environment monad on the simply-typed lambda calculus, using the following three equations, where $r$ is some fixed type, $\alpha$ is any type (I subscript some terms with their ...
79 views

### Lambda Calculus Conversion

How can I take a Haskell data type or function (eg fold, list, String, zip) and convert or translate it to a lambda calculus abstraction? Example: If sum computes a sum of all elements in a list, and :...
48 views

### Inhabitation of STLC is in PSPACE

Urzyczyn: Inhabitation in Typed Lambda-Calculi (A syntactic approach) gives a proof that STLC inhabitation problem is in PSPACE (section 2, lemma 1). I don't understand certain aspects of the proof: ...
49 views

### Tried to derive the Z combinator and instead derived another

I was working to derive the Z-Combinator by starting with the factorial function and ended up deriving a different fixed-point combinator. What did I derive? Did I make a subtle mistake? Here are the ...
121 views

### alpha equivalence of lambda calculus

I am pretty new in λ calculus. And I am now trying to understand Alpha equivalence. Basically can I think it in this way: as long as I make sure all the bound variables and their corresponding ...
66 views

### Understanding $\lambda \mu$-calculus in more programming way

I am learning $\lambda \mu$-calculus (self-study). I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
42 views

### Lambda calculus without free variables is as strong as lambda calculus?

First question: How would one prove that by removing free (unbound) variables from lambda calculus, and allowing only bound variables, its power is not reduced (it is still Turing-complete) ? Second ...