# Tag Info

### I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false

A phrase like "it is not possible to encode product types in the simply-typed $\lambda$-calculus (without product types)" means: it is not true that for every type $A$ and type $B$, there ...
• 661
Accepted

### What exactly is delta reduction?

Sadly, there is no clear consensus on what $\delta$-reduction is, other than the Greek letter $\delta$ being similar to the Latin "d" which also happens to be the first letter of "...
• 8,233

### Why Normalisation by Evaluation needs to use a different representation of programs?

It is good to know some basic facts about section-retraction pairs. Suppose $f : X \to Y$ of and $g : Y \to X$ are maps such that $g \circ f = \mathrm{id}_X$. We say that they form a section-...
• 30.9k

### What is a simple explanation and example of de Bruijn indices?

I suppose I do not understand why the definition needs multiple lambda terms M, N, …. Wouldn’t you just use de Bruijn indices for a single lambda term, such as lambda x . x + x? This is merely a ...
Accepted

### Closures break induction in correctness proof of interpreter

You must strengthen the theorem to be proved by induction. In the $e_1e_2$ case, the current induction hypothesis just tells you that $e_1$ reduces to a closure, but not anything more about how the ...
• 470
Accepted

### Is my understanding of Eta reduction correct?

returns a function and two variables No, it returns the result of applying the function to these two arguments. This result of course uses the arguments. Instead, consider this. I don't know what ...
• 3,192
Accepted

### Expression with fastest growth in lambda-calculus

Ok, I want to interpret this question as: what is the biggest growth rate a term $t$ of size $|t| = C$ can have, after $n$ $\beta$-reductions (as a function of $n$). There are several different ...
• 8,233

### Valid Lambda Expressions

What do you call a valid λ-expression? This is not a standard concept. Anyways, λ-expressions are the terms built inductively as follows: given a fixed set $V$ of variables, all $x \in V$ are λ-...
• 141

### $xx$ application in lambda calculus

You're right: $xx$ is the application of $x$ to $x$. But this is not a problem as long as you remember that you're only dealing with syntax here: $x$ is a term, $x$ is another term, so $xx$ is a term. ...
• 141

• 2,192
1 vote

### (how) is assignment or binding possible in purely functional languages?

The lambda calculus has names for the parameter (bound variable) to a lambda abstraction. That is the only mechanism or introducing names. Apart from that, there are no names in the lambda calculus. ...
• 162k
1 vote

### Is it actually the case that $Yg \to_\beta g(Yg)$?

I think it is technically incorrect that $Y g →_β g(Yg)$ using the definitions you've given. However, the one step $β$ reduction of $Yg$ is a fixed point of $g$ under reduction. Since the things you'...
• 2,727
1 vote

### What exactly is delta reduction?

Even though @cody already gave a great answer, I would maybe simplify it a bit, as the comparison with let might be confusing for beginners. With one sentence: The substitution of a defined symbol ...
• 111
1 vote

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

$U = λxλy·y(xy)$ is the fixed point of $Y$ and $Y$ is the fixed point of $U$. How, and in what sense, I describe here: Equality Of (Infinitary) Lambda Terms.
• 349
1 vote
Accepted

### Equality of lambda terms which do not have normal form

By extending the λ-calculus to allow for infinite λ-terms and infinite reductions. Then you may assert that both $Y f$ and $Θ f$ have $f(f(f(⋯)))$ as their normal form and, thus, that Y = λf·Yf = λf·...
• 349
1 vote

### how to solve this lambda expression with free variable/s

You're asking what the value of $λx·xy$ as if the expression, itself, were a math problem to somehow be solved. The situation is similar to asking what the value of "4/3" is, as if it were ...
• 349

Only top scored, non community-wiki answers of a minimum length are eligible