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
0 votes
0 answers
38 views

Set theoretic definition of terms of the untyped lambda calculus

I am trying to translate the following definition (in Agda) of intrinsically scoped terms of the untyped lambda calculus into more mathematical (in particular set theoretical) notation: ...
user11718766's user avatar
1 vote
0 answers
18 views

What is the correct way to encode the 2nd projection of a dependent pair type?

Consider the following Church-encoded definition for a dependent pair type (a.k.a. existential type) in a pure type system such as the Calculus of Constructions: $$\operatorname{Exists} \;\; := \;\; \...
cp289's user avatar
  • 11
2 votes
0 answers
41 views

Relating the Semantics of Church's Simple Type Theory to Dependent Type Theory

I'm looking at the 'standard' semantics of Church's simple type theory/simply typed lambda calculus (see for example section 2 here or pp. 194-196 in the January 2024 version of this), and I'd like to ...
user837242's user avatar
0 votes
0 answers
56 views

On the definition of 'dependent functions' in the set-theoretic semantics of dependent product types

I'm working in a framework (see e.g. this) where a context $\Gamma$ is interpreted as a set $[\![{\Gamma}]\!]$, a type $A$ in context $\Gamma$ is interpreted as a family of $[\![{\Gamma}]\!]$-indexed ...
user837242's user avatar
2 votes
0 answers
87 views

(weak necessity) proof a collection is closed under Modus Ponens from prior assumptions

I am looking for help understanding Exercise 7.3 from A Philosophical Introduction to Higher-order Logics by Bacon. The ultimate goal of the exercise is to prove the right-to-left direction of the ...
C D's user avatar
  • 43
1 vote
1 answer
25 views

Does the opposite direction of alpha congruence in applications hold?

The forward direction is: if $s \equiv_\alpha s' \land t \equiv_\alpha t'$, then $st \equiv_\alpha s't'$. I'm wondering if this holds: if $st \equiv_\alpha s' t'$ then $s \equiv_\alpha s' \land t \...
Kleon's user avatar
  • 11
0 votes
0 answers
19 views

A normal form for a chaotic combinator term?

Here is the term: $M M C$, where $M = S (S S) S$, which involves the combinators $C = λxλyλz((xz)y)$ and $S = λxλyλz((xz)(yz))$. What does $M M C$ reduce to, under β-equivalence? Or ... if its β-...
NinjaDarth's user avatar
0 votes
0 answers
58 views

Could someone check my attempt at a proof of a theorem in the lambda calculus?

I am working through Barendregt's "The Lambda Calculus" and attempted a proof of a proposition in chapter 2 § 1. Definitions - $$ \begin{align} \\ \text{A $context$ C[ ]}&\text{is a term ...
ZarakshR's user avatar
  • 111
3 votes
2 answers
64 views

Defining the Y combinator in terms of S, K and I

We know that the Y-combinator is defined as: $$\text{Y}:=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$ Wikipedia says :$$\text{Y}:=\text{S(K(SII))(S(S(KS)K)(K(SII)))}$$ Now the question is: What ...
Soham Saha's user avatar
  • 1,204
0 votes
1 answer
27 views

Can a CL-term have multiple fixed points?

Given a CL term $E$, can there exist multiple non-equivalent fixed points for $E$? I think: any fixed point of $E$ can be expressed as $Y(E)$, this expression cannot reduce to multiple non-equivalent ...
Soham Saha's user avatar
  • 1,204
2 votes
1 answer
47 views

Checking equivalence of combinatorial terms.

Due to some context, I have reason to believe that S(K(SII)) and SSI are actually equivalent CL terms. This is my attempt at a proof (assuming a and b to be arbitrary CL terms): $$\text{S(K(SII))ab = ...
Soham Saha's user avatar
  • 1,204
4 votes
2 answers
158 views

Mutually recursive definition of the terms to nonreqursive defenition with Y combinator.

Can't solve this task: Let there be a mutually recursive definition of the terms ${foo}$ and ${bar}$. In general, it can be written as $$ {foo} = P {foo} {bar} $$ $$ {bar} = Q {foo} {bar} $$ Here $...
replikeit's user avatar
  • 171
1 vote
1 answer
65 views

Defining Church numerals in higher order logic.

I'm looking for some help with Exercise 5.11. in Bacon's A Philosophical Introduction to Higher-Order Logics. Construct an explicit definition of the finite Church numerals, Num$_{\sigma}$, in higher-...
C D's user avatar
  • 43
3 votes
1 answer
56 views

complement of a property in the lambda calculus

I'm trying to demonstrate that the complement of the complement of a property is equal to the property itself using $\lambda$ notation, i.e. if $G=\lambda x(\neg Fx)$ and $R=\lambda x(\neg Gx)$, then ...
saulkripke321's user avatar
3 votes
1 answer
60 views

Michell FPL 2.3.5 (observable types)

(a) Show that the relation of observational equivalence remains the same when changing the observable types of pcf from nat, bool to nat. (b) Further show that changing from nat,bool to nat, bool, ...
emesupap's user avatar
  • 645
2 votes
0 answers
35 views

Where do recursive types fit in the lambda cube?

A way to extend the simply-typed lambda-calculus $\lambda_\to$ is to consider recursive types of the form $\mu\alpha.\tau$ (see for example http://www-verimag.imag.fr/~iosif/LogicAutomata07/type-...
user avatar
1 vote
1 answer
57 views

Combinatory Logic Problem With Partial Reductions

I'm working through Bacon's Philosophical Introduction to Higher Order Logic. I am looking for help on the following problem: Exercise 3.17 Calculate the following, assuming that $\wedge : t \to t \...
C D's user avatar
  • 43
3 votes
2 answers
123 views

Prove that the normal form of a closed term in the STLC of simple type contains no lambdas or applications.

Suppose that we have a closed term x:t in the simply typed lambda calculus (STLC) (i.e. this term does not contain any free variables). You can use the terminology ...
martin's user avatar
  • 185
4 votes
1 answer
216 views

Can irrational numbers be represented EXACTLY in lambda calculus?

We know that $0 = \lambda f. \lambda x. x$, $1 = \lambda f. \lambda x. f(x)$ and so on, with signed numbers representable as a natural number and $0$, and rational numbers can be represented as pairs ...
3-1-4-One-Five's user avatar
4 votes
1 answer
75 views

Lambda calculus function with unrestricted domain and nontrivial finite range?

In the untyped lambda calculus, one of the first encountered expressions is: $F = Const(I) = \lambda x.\lambda y.y$ It is easily seen that a property of this expression is that the set of possible ...
BadZen's user avatar
  • 201
10 votes
0 answers
261 views

Turing-complete recursive function using only $a^b$ and $\log_b a$

Edit: Below, I establish this for $\{\log x,x^y,-1\}$. It occurs to me that you can trade the requirement of including $-1$ for the ability to use a log with any base. This follows because given an ...
Trevor's user avatar
  • 6,022
1 vote
1 answer
50 views

How do interpret $x \lambda y . \lambda z . x$?

I am not sure how to interpret this term. My first thought is that it is this an application of $x$ to $\lambda y.\lambda z.x$ Is that the correct interpretation or is it not reducible?
mcmapple's user avatar
  • 121
3 votes
0 answers
80 views

Predecessor function in λI-calculus

The $\lambda_I$-calculus is a restricted version of the usual $\lambda$-calculus. The set of expressions in this restricted calculus, $\Lambda_I$, can be defined inductively: If $x$ is a variable, ...
André Batenburg's user avatar
0 votes
1 answer
113 views

Fixed-point of a function and an inverse problem

This is perhaps a theoretical computer science question. Please help redirect appropriately. The question is about mental processes involved in discovering a solution. Consider an iterative higher-...
Kedar Mhaswade's user avatar
0 votes
0 answers
82 views

Combinators that form a 1-symbol basis of alternating associative combinatory logic

It is known that the combinators $S,K$ form a basis for lambda calculus. It's also known that the iota combinator $\lambda x.((x S) K)$ is a basis. Chris Barker found that the iota combinator allows a ...
Legendary Wizard's user avatar
1 vote
0 answers
131 views

isDivisible function in lambda calculus for Church numerals

After trying without success for several days to find a proper software/website that can correctly simplify lambda terms (see this question), I ended up deciding to use JavaScript to do the same. The ...
Soham Saha's user avatar
  • 1,204
2 votes
1 answer
86 views

Checking equivalence of lambda terms

I was trying to develop an alternative to the Church encoding for the predecessor function for Church numerals. What I came up with was: $$pred := λn.first (n (λp.second (p)(pair (succ (first (p))) ...
Soham Saha's user avatar
  • 1,204
1 vote
0 answers
57 views

Is this $\alpha$-conversion correct?

I found this $\alpha$-conversion below in a certain book: $(\lambda x. x(\lambda z. xy)) = \alpha (\lambda z. z(\lambda x. zy))$ Well... this seems wrong to me, since $z$ is a binding variable in ...
Paulo Argolo's user avatar
  • 4,220
0 votes
0 answers
89 views

If closed lambda calculus expression $M$ doesn't have a normal form, can $λx.λy.(M (x y))$ have a normal form?

I'm trying to solve the following problem, but I'm not sure if it's actually possible/true: "Let $M$ be a closed pure lambda term without normal form. Prove that $\lambda x.\lambda y.(M (x y))$ ...
Legendary Wizard's user avatar
0 votes
0 answers
32 views

Induction on the length of a lambda-term

Let M be a λ -term, with length m, that is: m = lgh(M). Well... I think "induction on lgh(M)" means the same as "finite induction on m". But I'm not sure. I ask for help.
Paulo Argolo's user avatar
  • 4,220
0 votes
0 answers
55 views

Why does alpha equivalence not apply to free variables?

It's mentioned in the book "Haskell programming from first principles" in the first chapter that one free variables don't have equivalence that is: $$ \lambda x.xy \overset{\alpha-\text{eq.}}...
tryst with freedom's user avatar
0 votes
0 answers
86 views

Lambda Calculus Equivalence and Call by name

I am new to lambda Calculus and wanted to understand the 2 following questions: ...
Ran123's user avatar
  • 3
2 votes
1 answer
62 views

Find an inhabitant for type $\phi$

I am studying from Sorensen's book (Lectures on the Curry-Howard isomorphism, ed. 2006) and there is a type that is said to be inhabited, but I need to find the inhabitant. However, I can't find it. ...
Νικολέτα Σεβαστού's user avatar
0 votes
2 answers
83 views

How do you formally show that “being a subterm of” is a transitive relation (on λ-terms)?

I see in a book on Type Theory the following definition of a subterm of a $λ$-term: We call $L$ a subterm of $M$ if $L ∈ \mathrm{Sub}(M)$. $\mathrm{Sub}(x) = \{x\}$, for each $x ∈ V. (V$ is the set ...
Paulo Argolo's user avatar
  • 4,220
2 votes
1 answer
71 views

SKI combinatory calculus, $M$ doesn't have a normal form. Find $(M S)$ that has a normal form

The problem is related to a similar question about lambda calculus. This question is about SKI combinatory calculus. I want to find a term $M$ without a normal form that will yield a term with a ...
Legendary Wizard's user avatar
0 votes
1 answer
35 views

Alpha conversion and free variables

I am studying lambda calculus from "Lectures on the Curry-Howard isomorphism" and I want to clear out a small detail in a proof using induction on the definition of alpha conversion. Alpha ...
Νικολέτα Σεβαστού's user avatar
0 votes
0 answers
49 views

Do you multiply or add when simplifying $λ$-expressions?

The question is to simplify this λ-expression $(\lambda x. x) (\lambda x. \lambda y. y x) 8 (\lambda x. x + 1)$ My current thinking is as follows: $(\lambda x. x) (\lambda x. \lambda y. y x) 8 (\...
James White's user avatar
1 vote
0 answers
127 views

Does Curry-Howard correspondence mean that everyone who writes a program is doing intuitionistic mathematics?

As far as I know, the first statement of the correspondence is between two formal theories named simply typed lambda calculus and intuitionistic propositional logic, which maps types to formulas and ...
Senmorta's user avatar
4 votes
1 answer
154 views

An overview of mathematical-logical approaches in formalizing natural languages

Crossposted on MathOverflow I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach), ...
Heleyrine Brookvinth's user avatar
0 votes
0 answers
29 views

Substitution of M in Beta Reduction (Lambda Calculus)

I am preparing for an exam where I have a Beta reduction question. The question goes as follows: $M=(\lambda xy.x(\lambda z.xyz))(\lambda x .xz )(\lambda y.ya)$ I have been working this out and ...
eoan's user avatar
  • 1
0 votes
1 answer
109 views

What is infinitary lambda calculus? [closed]

I've recently discovered the existence of infinitary lambda calculus, or infinite lambda calculus, and am interested but unclear about some of its properties. So what is infinitary lambda calculus and ...
Steve Mucci's user avatar
3 votes
1 answer
97 views

Using beta reduction on $ \lambda y. ( \lambda x. \lambda y. y x)(\lambda z. y z)$

I have a few questions regarding this exercise: $$ \lambda y. ( \lambda x. \lambda y. y x)(\lambda z. y z)$$ This is what I have come up with: $ \lambda y. ( \lambda x. \lambda \color{red}u. \color{...
john doe's user avatar
  • 893
2 votes
1 answer
28 views

$(\lambda z. zy)(\lambda z. zy)$ - reducing using $\beta$ reduction and $\alpha$ conversion

Good day . I need to reduce the following expression of lambda calculus: $(\lambda z. zy)(\lambda z. zy)$ Now, since I am having the variable $y$ in both the left and right pair of parentheses, I ...
john doe's user avatar
  • 893
1 vote
2 answers
33 views

Beta reduction on $(\lambda x . xu)(\lambda z. wzwz)yv$

I need to perform a reduction on the following lambda expression $(\lambda x . xu)(\lambda z. wzwz)yv$ This is what I have done so far: $(\lambda x . xu)(\lambda z. wyvwyv) = wyvwyvu$ However, my ...
l0ner9's user avatar
  • 623
1 vote
1 answer
71 views

Substitution in a complex lambda calculus formula

I have the following lambda expression: $$( (y \lambda x \rightarrow \lambda y \rightarrow f y) (\lambda f \rightarrow f y z) )[y := f x]$$ So, my questions are, I see $y$ before a lambda abstraction,...
F. Zer's user avatar
  • 2,357
1 vote
0 answers
52 views

Lambda calculus: "succ expressions" are all polynomial functions on Church numerals?

The specific definition of $\mathsf{succ}$ for Church numerals $$ \mathsf{succ} = \lambda n f x. f (n f x) $$ seems to have an interesting property when applied to itself: (here, all expressions on $n$...
Bubbler's user avatar
  • 291
1 vote
2 answers
143 views

Simplyfing $(\lambda y. z)((\lambda x. x x)(\lambda x. x x))$

I need to simplify this expression. $(\lambda y. z)((\lambda x. x x)(\lambda x. x x))$ However, what's interesting to me are two things: Should I start simplifying $((\lambda x. x x)(\lambda x. x x))$...
l0ner9's user avatar
  • 623
3 votes
1 answer
72 views

How to convert lambda expressions into morphisms in a Cartesian Closed Category?

I'm trying to understand how named variables relate to function composition. So, in a program, it's useful to have named intermediate variables, so you can use them multiple times in the future: ...
Polymer's user avatar
  • 423
3 votes
1 answer
104 views

Proving that the Curry fixed point combinator y and the Turing fixed point combinator θ cannot be proved equal in λβ

$y = λf.(λx.f(xx))(λx.f(xx))$ $θ = (λxy.y(xxy))(λxy.y(xxy))$ I'm trying to prove that $y \neq \theta$ in λβ. My idea was to assume the contrary, then by Church - Rosser, there exists some $u$ s.t. ...
SVMteamsTool's user avatar
0 votes
1 answer
94 views

Lambda function which generates a sequence

Consider this sequence of lambda functions: $\lambda xy. yxy$, $\lambda xyz. zxyz$, $\lambda xyzw. wxyzw$, etc. I would like some lambda function $g$ such that when $g$ is applied to $n$, it returns ...
weux082690's user avatar

1
2 3 4 5
14