# Questions tagged [lambda-calculus]

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

438 questions
Filter by
Sorted by
Tagged with
73 views

### Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
52 views

### “not provable”, what does this to do with unification?

I found one interesting point in nominal unification. Just after proposition 2.16 of Nominal Unification by Urban, Pitts, and Gabbay, it said the following, which I found confusing: For non-ground ...
126 views

### Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection

Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category. I was wondering if in such context it is ...
281 views

### Lambda Calculus in Rewriting systems

How to do or implement Lambda Calculus in a Rewriting systems? Rewriting systems are Turing complete. But I can't figure out how to do lambda calculus or functions with them.
127 views

### Is this a valid representation of a function in Lambda Calculus?

Let's say I want to define a function: This function multiplies an input by two, adds one to this integer, then divides it by two in that order. f represents the multiplication, g represents the ...
141 views

### Functorial type constructors in System F

I have come across the claim that all basic data types in System F, such as Bool, Nat, and List(U), can be expressed in the form $\forall \alpha (((T\alpha \rightarrow \alpha) \rightarrow \alpha)$, ...
455 views

### What can you do with lambda calculus if you aren't allowed parentheses?

Is there a concise/existing way to denote the expressive power of "lambda calc without using parentheses/tree-of-expressions/application-order-restructuring anywhere"? Can you do without them/...
150 views

### Nominal unification: How this lemma is proved?

I was reading nominal unification paper. I could not understand the proof of a lemma. The paper is here nominal unification. The lemma is following. $\sigma$ is a substitution, $\pi$ is a permutation ...
363 views

2k views

### Difference between beta reduction and substitution

I can not see the difference between beta reduction and substitution. For example: (+ x 1) [x -> 2] Here I can do the substitution, replace the variable x ...
97 views

### Lambda calculus application [closed]

I have a function application: E1 E2 Can someone please show me an example, how to execute function?
40 views

### Why it converts to T

The AND function in the lambda is: and = (Ī» a. Ī» b. a b F) I have following expression: and T T then the result will ...
131 views

### Problem with Church numerals evaluation

I am trying to understand Church's Numerals for 4: $$4 = \lambda f.\, \lambda x.\, f f f f x\,.$$ This will be evaluated in the following order: $$\lambda f.\, \lambda x.\, (f (f (f (f x) ) ) )\,.$$...
379 views

### What is the point of this lambda expression?

Let's take this lambda expression : $\lambda\:x \:\ast\:x\:2$ that "computes" x * 2. From what I understand, $\ast$ is a constant operator, but since its nothing ...
391 views

### Intuitive explanation of neutral / normal form in lambda calculus

It is possible to distinguish Normal terms which don't contain beta redex as a sub-expression, from others like so ...
199 views

85 views

### Understanding A Recursive Definition of CL-Terms in Combinatory Logic

From page 26 of Lambda-Calculus and Combinators: Definition 2.18 (Abstraction) For every CL-term $M$ and every variable $x$, a CL-term called $[x].M$ is defined by induction on $M$, thus: (a)...
106 views

### Is there a correspondence between the syntaxes and the type systems of programming languages?

I was reading the first chapter of Robert Harper's Practical Foundations for Programming Languages in which it introduced abstract binding trees, aka abt. It seems pretty like typed lambda calculus. ...
200 views

### ground terms in logic and $\lambda$-calculus?

What are the differences of ground terms in first-order logic and higher-order logic? I found on the Wikipedia: "In mathematical logic, a ground term of a formal system is a term that does not ...
105 views

### Why is the word “calculus” used to describe systems of logic and computation?

Why is the word "calculus" used in this context? The reason I ask is because these usages of "calculus" seem unrelated to the far more popular use of "calculus" in "differential calculus" and "...
1k views

### What is the difference between strong normalization and weak normalization in the context of rewrite systems?

In the context of rewriting systems, how does strong normalization differ from weak normalization?
203 views

### How is this expression a valid lambda expression?

Can you explain how this expression follows the grammar of the lambda calculus? $$\lambda x.x((\lambda y.yy)x)x = Ī»x.x(xx)x$$ I am not sure why we have the parentheses following the $.x$ (on both ...
213 views

### What is a super universe?

I'm reading this well-known paper On Universes in Type Theory. At first I expected something similar to SetĻ in Agda, but it turns out that it's even something more ...
2k views

### Lambda calculus lists construction explanation

I have the following notes that introduce how lambda calculus handles lists. They go as follows: A list is something we can match on and deconstruct if it is not empty: ...
120 views