# Questions tagged [lambda-calculus]

For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

423 questions
Filter by
Sorted by
Tagged with
52 views

### Ideas regarding lambda calculus

I want to work on lambda calculus as part of my MA thesis. What would be a suitable problem for me to tackle? I mean, what are the current research topics related to lambda calculus? What new results ...
51 views

### Given an inhabited type in simply-typed lambda calculus (w/no basics, just variables), is there a combinator of that type that is no longer than it?

Apologies if I've got some of the terminology here wrong, typed lambda calculus is a bit new to me. Let's say we've got a type in simply-typed lambda calculus with no basic types (functions and type ...
176 views

### What axioms can be added to $S,K$ combinator algebra without making it collapse into triviality?

My understanding is that if you start with the free magma on two generators (call them $S$ and $K$) and then take a quotient with respect to the usual $S$ and $K$ equivalence rules ($Sfgx = fx(gx)$ ...
38 views

### Have I written this statement correctly?

I have written the following intentionally false statement: f(x:t) ⊢ y:u ∴ u = t This is intended to express that: x of type t causes y of type u, therefore u is ...
22 views

### Weak Normalization of Beta-Reduction on typable lambda-terms

I have to directly show weak normalization of the β-reduction on typable λ-terms, without showing (a property that entails) strong normalization. Hint: an idea analogous to that for the cut ...
59 views

27 views

### Lambda calculus expression evaluation.

I ran across the following lambda calculus example problem plusTwo = 𝜆n.successor(successor n) 4 plusTwo 2 = 10 I'm having trouble understanding how the answer ...
40 views

### What is the subterms of $M\equiv (\lambda x\cdot yx)(\lambda z \cdot x(yx))$?

Using this Definition (Subterms): The subterms of a term M are defined by induction on $|M|$ as follows: an atom is a subterm of itself; if $M\equiv \lambda x \cdot P$, its subterms are $M$ and all ...
46 views

### Parentheses placement and identifying redexes in a lambda expression

I'm struggling to understand how to identify redexes in a lambda expression. I've been given the following expression and asked to identify all redexes (𝜆𝑥.(𝜆𝑥.𝑥)𝑥)(𝜆𝑥.𝑥)𝑥 I understand ...
46 views

81 views

### Is there generalization of the natural numbers?

Natural numbers are defined inductively https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab30 as s(s(...s(0)...)). Such definition is nothing special, especially when one can ...
29 views

### Beta-Reduction exercise with pairs in Lambda Calculus

I'm doing some simple exercise about Lambda Calculus but i have doubt about this beta-reduction. Let $$<u,v>= \lambda p((p)u)v$$ a pair in Lambda Calculus. Prove that for every lambda term M ...
230 views

### A Question About the Order of Learning from the Book “Lectures on the Curry-Howard Isomorphism” (1998)

I'm learning from this book: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf (Lectures on Curry-Howard Isomorphism - 1998 version) for some project. And due to time constraints, I ...
50 views

### What's the Meaning of the Notation $\langle \mathbf{\cdot} , \mathbf{\cdot} \rangle$ in $\lambda$-Calculus?

I'm learning $\lambda$-calculus from this book: Lectures on the Curry-Howard Isomorphism (1998 version) (https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf), and in page 17, definition 1....
50 views

57 views

### Question About Part of the Proof of a Lemma to the Church-Rosser Theorem in “Lectures on the Curry-Howard Isomorphism”(1998)

Before I will ask my question, I would refer you to the relevant information in the 1998 version of the book "Lectures on the Curry-Howard Isomorphism" (https://disi.unitn.it/~bernardi/RSISE11/Papers/...
42 views

### Question About the Substitution of $N$ for $x$ in a $\lambda$-term, as Defined in “Lectures on the Curry-Howard Isomorphism” (1998)

I'm learning from the 1998 version of "Lectures on the Curry-Howard Isomorphism" book, since it's freely available online (https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf) as opposed ...
75 views

### Terms in the lambda calculus

The formal definition of the lambda calculus I am seeing here reads: The class of $\lambda$-terms is defined inductively as follows: Every variable is a $\lambda$-term. If $M$ and $N$ are ...
23 views

### Calculi of Lambda Conv: Question on Abstraction

I'm reading Page 4 of the Calculi of Lambda Conversion by Church. BI is 1, since it is the operation of composition with the identity transformation, and thus an iden- tity operation, but one ...
316 views

### “Recursive types for free!” — But doesn't this contradict the fact that $\mathbb{N} \notin \mathbf{FinSet}$?

From what I understand based on Philip Wadler's comment, polymorphic lambda calculus has least fixed points for all its covariant endofunctors. Here's a quote: Thus, it is safe to extend the ...
72 views

### How do we know whether all elements of $[A\to B]$ can be represented as computable functions?

While working through Barendreght's book on the Lambda Calculus, and Abramsky's notes on Domain Theory, I had the following realization: It's often stated that Domain Theory provides a semantics for ...
22 views

### Lambda Calculus and Abstract Reduction systems

I'm having a hard time understanding Lambda Calculus and I have a two questions that I'm not sure how to do/what they mean. Below we are supposed to use Abstract Reduction Systems. Define an ARS (N×N,...
43 views

### Lambda calculus: evaluation by value would not terminate but normal evaluation terminates

I'm wondering if it is possible that evaluation by value would not terminate but normal evaluation terminates. Because in normal evaluation we will evaluate until we reach a normal form meaning that ...
75 views

### Lambda-Calculus: binding precedence

I'm utterly confused and hope to find clarification here. I came across a $\lambda$-calculus Interpreter by Liang Gong (who ever that is :)) claiming to be of California University of Berkley. Link: ...
43 views

### Proof term for predicate calculus.

Proofs of propositional calculus may be written in simple typed lambda calculus(λ→). (as shown on p.52-53 in https://www.cs.ru.nl/~freek/talks/lc-2012/lambda5.pdf ) I think that this calculus may be ...
81 views

### Finding inhabitants in Lambda P

I found two examples in some lecture notes online and I can't follow their approach on the solution. Maybe someone can help. First they translate from predicate logic to $\lambda$P and then they give ...
55 views

### Is this Church encoding of lists correct?

Types and Programming Languages by Pierce introduces Church encoding of lists in Exercise 5.2.8 on p63 and p500: ...
62 views

42 views

### Lambda Calculus and arithmetic hierarchy

Can lambda calculus be used to define classes $\Sigma_n$ in the arithmetic hierarchy? What I'm looking, in particular, is if lambda calculus can be used for studying limit computability.
84 views

### Is this proof of Barendregt's Substitution Lemma (lambda calculus) correct?

So I have attempted to prove the lemma mentioned in the title, but I am not sure if it is correct. In the book I am reading, the Lemma was given without proof. We were given the following definitions:...
126 views

### In Lambda calculus, Is there some alternative equivalence to $\eta$ conversion?

In Lambda calculus, is there some alternative equivalence to $\eta$ conversion? I am reading Hendrik Pieter Barendregt's Introduction to Lambda Calculus. On Page 11, I saw $\beta$-reduction, $\alpha$...
88 views

### Beta reductions' evaluation order

Could you please help me understand $\beta$ reductions' evaluation order. I've seen the most common approaches are Applicative : reduce the leftmost, innermost $\beta$ redex first. Normal : ...
I've got a few questions about $\lambda$ calculus' syntax and how to interpret it. Most of these questions sparked from reading this notes. First thing first, an application 's syntax is defined ...