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.

Filter by
Sorted by
Tagged with
1
vote
0answers
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 ...
3
votes
1answer
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 ...
9
votes
2answers
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)$ ...
0
votes
1answer
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 ...
0
votes
0answers
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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 ...
2
votes
1answer
46 views

Identifying redexes in a lambda expression

I've been given the following expression and asked to identify all redexes \begin{align} (𝜆x.xx)(𝜆x.xx)(𝜆x.xx)(𝜆x.xx) \end{align} The example key gives the first part of the expression $(𝜆x.xx)(𝜆...
2
votes
1answer
341 views

Lambda Calculus, applicative vs normal order

I just started learning lambda calculus, and i have this question to do with normal order and in applicative order: (λfx.f (f x))(λfx.f (f x)) f x In normal ...
0
votes
0answers
24 views

How to determine a representation of Fold function in Lambda Calculus?

I've to determine that function $F$ : $$(((F)g)x)[b_1 ... b_n] \rightarrow_{\beta} [g(b_1,x) \: g(b_2 \: g(b_1,x)) ... g(b_n,g(b_{n-1},g(b_1,x)))]$$ where $g$ is a function that return a boolean $b$ ...
1
vote
1answer
30 views

(Functional) space of all lambda types (algorithms)?

The most simplest notion of the algorithm is some kind of function with input and output. Input and output can be very sophisticated mathematical objects (not only numbers), but the is irrelevant, ...
2
votes
0answers
41 views

Automated discovery of interesting theorems by searching motifs in words (e.g. Coq lambda calculus) - grammatical notion of reverse mathematics?

Proof assistant Coq allows to represent any theorem as the lambda type (whose proof is the lambda term) (there are other proof assistants like Isabelle/HOL, Lean, etc. that allows similar grammatical ...
0
votes
0answers
19 views

How to find a lambda term to complete a function?

I tried to complete this exercise but i stopped... Defining a $ \lambda $-term M such that: $$(<M,u>)<M,v> \: \simeq_{\beta} \: <M,u>$$ I chose $M=\lambda m \lambda a \lambda b \...
0
votes
1answer
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 ...
2
votes
1answer
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 ...
2
votes
1answer
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 ...
1
vote
2answers
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....
2
votes
1answer
50 views

what are the cases that we can say that the lambda term is not typable?

We have some cases that we say lambda term is not typable for example $Ω=(λx.xx)(λx.xx)$. I got a question about type of the term $λxab.xa(xb)$ Here, the first occurrence of $x$ receive $a$ and $...
2
votes
1answer
37 views

lambda calculus type assigned problem

we have $\lambda xabc.xa(xbc)$ and we should give a type for it can we assign $a$ and $b$ to the same symbol ? like here $a$ and $b$ should be same type for example $\alpha$ so we can continue ? $a,b =...
2
votes
1answer
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/...
2
votes
1answer
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 ...
6
votes
1answer
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 ...
1
vote
1answer
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 ...
3
votes
1answer
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 ...
4
votes
0answers
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 ...
1
vote
0answers
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,...
4
votes
1answer
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 ...
3
votes
1answer
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: ...
1
vote
1answer
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 ...
0
votes
1answer
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 ...
1
vote
1answer
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: ...
4
votes
1answer
62 views

Lambda calculus substitution rule explanation

One of the rules for the definition of substitution in the lambda-calculus is: $$[x \mapsto s]y = y \ \text{ if } \ x \neq y$$ But how can $x = y$? After all I am not substituting $y$ for $s$, but $...
0
votes
1answer
60 views

How do I simplify these lambda calculus equations?

How do I solve these lambda calculus equations? $\lambda x y z . x y (z x)$ $\lambda x y z . x y (z x y)$ For 1, is this correct? $xy[xyz := zx] = x$?
0
votes
0answers
25 views

Is this lamda abstraction created as a generator of a recursive function?

In Lambda calculus, a recursive function $f$ is obtained by $$ f = Y g $$ where $Y$ is the Y combinator and $g$ is the generator of $f$ i.e. $f$ is a fixed point of $g$ i.e. $f == g f$. In The ...
1
vote
0answers
107 views

How shall I understand the definition of `let` in mathematics?

let as used in programming languages is defined in lambda calculus as per https://en.wikipedia.org/wiki/Let_expression#Let_definition_defined_from_lambda_calculus ...
1
vote
1answer
47 views

How to reduce these equations with beta reduction - lambda calculus

How do I beta reduce these equations. My attempts are below the questions. (λy.zy)a = λy[y:=a].zy = λa.za (λz . zz)(λy . yy) = λz[z:=λy . yy].z z = (λy . yy)(λy . yy) = (λy[y:=λy . yy].yy) = (...
1
vote
0answers
49 views

Is anything wrong with this proof idea for showing that evaluation in the simply-typed lambda calculus always halts?

Consider the simply-typed lambda calculus over some set of base types, with call-by-value evaluation semantics. (Exactly what is discussed in Types and Programming Languages, in case it matters -- I'm ...
3
votes
2answers
209 views

How can types represent both sets and propositions in Lambda calculus?

There is an interpretation of Lambda calculus that views a derivable statement $\Gamma \vdash x : A$ as the proposition $A$ with $x$ as "proof" of $A$. However, there is another interpretation in ...
4
votes
0answers
72 views

Relationship between the semantics of simply typed lambda calculus and combinatory logic

The simply typed lambda calculus has a class of extremely intuitive models where each basic type $\sigma$ is modeled by some set $[\![\sigma]\!]$, and a complex type $\sigma\rightarrow\tau$ is then ...
4
votes
1answer
94 views

Are there recursive types in the theory of simple types? If not, how do I prove it?

In the book I am reading, the set of simple types $\mathbb{T}$ is defined by: If $\alpha \in \mathbb{V}$, then $\alpha \in \mathbb{T}$ If $\sigma, \tau \in \mathbb{T}$ then $(\sigma \to \tau) \in \...
2
votes
0answers
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.
3
votes
1answer
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:...
4
votes
2answers
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$...
4
votes
1answer
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 : ...
0
votes
0answers
53 views

Lambda calculus' syntax disambiguation

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 ...
3
votes
1answer
131 views

Beta normal form for the following expression

I was recently reading "Lambda calculus and combinators" by J.R. Hindley and J.P Seldin. In the book at some point we encounter the following reductions : $(\lambda x.x)v$ $(\lambda x.xxy)(\...
2
votes
1answer
44 views

Beta reduction result

I'm not understanding how to solve the following beta reduction : $$ (\lambda n.\lambda m.\lambda f.\lambda x.(n\,\,\,f)((m\,\,\,f)\,\,\,x))(\lambda f.\lambda x.ffffx)(\lambda f.\lambda x.fx) $$ My ...
1
vote
1answer
103 views

Doesn't cut elimination make intuitionistic logic equivalent to classical logic?

Suppose we have a proof by contradiction of $A$, meaning we've proven $(A \to \bot) \to \bot$. If we eliminate all cuts in the proof, then the last step of the proof will be an implication ...

1
2 3 4 5
9