Skip to main content
7 votes

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 ...
varkor's user avatar
  • 661
4 votes
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 "...
cody's user avatar
  • 8,233
3 votes

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-...
Andrej Bauer's user avatar
  • 30.9k
3 votes

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 ...
Jean Abou Samra's user avatar
3 votes
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 ...
Li-yao Xia's user avatar
3 votes
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 ...
Alexey Romanov's user avatar
2 votes
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 ...
cody's user avatar
  • 8,233
2 votes

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 λ-...
sparusaurata's user avatar
2 votes

$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. ...
sparusaurata's user avatar
2 votes

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

You're looking for Church encodings, which are encodings of type constructions and datatypes in the polymorphic $\lambda$-calculus. That is, apart from having function types $\to$ we also need $\...
Andrej Bauer's user avatar
  • 30.9k
2 votes
Accepted

Lambda Calculus vs Turing Machine

The short answer is that every computation describable in lambda calculus can be computed on a turing machine, at the same time every Turing machine program can be converted into a lambda calculus. ...
ratchet freak's user avatar
2 votes

Adding type constructors to universes

$Γ.\mathrm{El}(a) ⊢ U\ \mathrm{type}$ is valid because $Γ ⊢ U\ \mathrm{type}$ is valid for all $Γ$. Just pick $Γ.\mathrm{El}(a)$ as the context. For one, there is no reason to have the $a$ in that ...
Dan Doel's user avatar
  • 2,727
2 votes

Indexing a list in Lambda calculus

Recall that a Church numeral $n$ is $λf.λx. f^n x$. When given arguments, it applies $f$ to $x$ $n$ times. So to index a list, we can apply the tail function to the list n-1 times, then get the head ...
confusedcius's user avatar
2 votes

"union" or "disjunction" in pure untyped lambda calculus

The usual way to encode coproducts is as: $$ι_1\ x = λk_1\ k_2.\ k_1\ x \\ ι_2\ y = λk_1\ k_2.\ k_2\ y$$ Matching is then, as you said, $[f,g]= λs.\ s\ f\ g$. The obvious problem with idempotence is ...
Dan Doel's user avatar
  • 2,727
1 vote

In what sense do universes solve the problem of not having type $\Pi_{A:\text{Type}}B(A)$?

$\mathrm{El}$ is how you get the type corresponding to a code. So, wherever you would imagine $A$ occurring in $B$, instead $\mathrm{El}(a)$ occurs. This makes $B$ into a family over the universe ...
Dan Doel's user avatar
  • 2,727
1 vote

$xx$ application in lambda calculus

in $\lambda x . f(xx)$, you are correct to say that $x$ is the variable of a lambda abstraction. However, a variable is simply a placeholder for the substitution that happens when the lambda ...
mell_o_tron's user avatar
1 vote

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

I suspect you're imagining $\text{let } x = E \text{ in } E'$ as describing a sequence of steps: take the thing described by $E$ and put it in the box labeled $x$, then proceed to the thing labeled $E'...
benrg's user avatar
  • 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. ...
D.W.'s user avatar
  • 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'...
Dan Doel's user avatar
  • 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 ...
tturbo's user avatar
  • 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.
NinjaDarth's user avatar
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·...
NinjaDarth's user avatar
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 ...
NinjaDarth's user avatar

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