Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [lambda-calculus]

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

1
vote
1answer
25 views

What are some concrete examples of what typed lambda constants are?

I was reading the following and found the following paragraph that I didn't understand: Let us also consider a set Σ of typed λ -constants, that is, pairs σ : t, where t is some type. Like for ...
0
votes
1answer
36 views

Handling epsilon productions in recursive descent parsing

I am working on a recursive descent parser for lambda calculus. In my grammar, after removing left-recursion, I am left with the following two productions: ...
0
votes
2answers
48 views

Multiple inputs in lambda calculus (Confusing example)

In a programming class I take, we briefly (very briefly) touched lambda calculus. I think I have a pretty good grasp of the basics now, but one example given I just don't understand. Am I missing ...
0
votes
1answer
37 views

Is this a correct grammar for untyped lambda calculus?

I am trying to write a recursive-descent parser for untyped lambda calculus. While researching the way of formulating the grammar, I managed to put together something like this: ...
1
vote
0answers
14 views

Combinatory Logic formula obtained from lambda term, proof?

I translated the following $\lambda$-term: $z(\lambda b.ba)(tt)(\lambda y.y)$ in the following CL formula: $z(CIa)(tt)I$ through the Markov algorithm. Now I'd like to prove the translation was ...
10
votes
2answers
86 views

Confluence of beta expansion

Let $\to_\beta$ be $\beta$-reduction in the $\lambda$-calculus. Define $\beta$-expansion $\leftarrow_\beta$ by $t'\leftarrow_\beta t \iff t\to_\beta t'$. Is $\leftarrow_\beta$ confluent? In other ...
2
votes
2answers
51 views

How does one show $(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$ in lambda calculus?

I wanted to show: $$ (\lambda x . (\lambda y.x))yx \equiv_{\beta} y $$ the definition of beta equivalence is on page 17 of these notes. I did a few attempts but got different things like $x$. I ...
0
votes
0answers
17 views

How do we show $\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$ in lambda calculus?

How do we show $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$$? I was going through the slides here and it asked to do the above but by page 16 of the slides we have not ...
2
votes
0answers
36 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
4answers
81 views

How does one formally show that two lambda functions are $\alpha$ equivalent?

I was going through the following slides and I wanted to show the following: $$ \lambda x. x \equiv_{\alpha} \lambda y . y$$ formally. They define a an $\alpha$-conversion on page 15 as follows: $$ ...
2
votes
2answers
72 views

Why is it that a lambda function requiring multiple input also requires multiple functions?

So I recently discovered lambda calculus and for the most part I understand it. However, one specific part of it that I cannot understand is this: Let's say we define a very simple function $$ I := \...
9
votes
5answers
2k views

Lambda Calculus Generator

I don't know where else to ask this question, I hope this is a good place. I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite ...
0
votes
1answer
29 views

How to find a function in Lambda Calculus?

Yesterday I have been trying to complete this exercise. I have to find: $$ ((map)l)t \simeq \lambda k \lambda x ((k)(t)t_1)....((k)(t)t_n)x $$ where $$l=\lambda k \lambda x ((k)t_1)....((k)t_n)x$$ ...
3
votes
1answer
39 views

Why does existence of predecessor imply adequacy of a numeral system?

I encountered this result when working with $\lambda$-calculus (so every element I mention here was a $\lambda$-expression there [1]), but I will express everything with, more understandable to ...
2
votes
1answer
80 views

Differences between Church and Scott encoding

I'm kind of new to lambda calculus and I found this Wikipedia article https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding The section Comparison to the Church encoding presents a short ...
1
vote
1answer
126 views

Reducing lambda expression to normal form

Can someone explain the steps to reduce $$ (\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x) $$ to $\lambda y. \lambda z.\...
2
votes
2answers
353 views

Encoding (binary) trees using lambda calculus

I'm new to lambda calculus, and I read all kinds of interesting stuff about encoding data types as functions. Church booleans, numbers and lists. https://en.wikipedia.org/wiki/Church_encoding Is ...
19
votes
0answers
353 views

Can a calculus have incremental copying and closed scopes?

A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
1
vote
1answer
79 views

How to transform lambda function to multi-argument lambda function and how to rewrite or approximate terms?

I am trying to do the formal semantics (Montague grammar, abstract categorial grammar) of natural language and encode the sentence John is boss. The type system has ...
1
vote
0answers
30 views

Call-by-push-value vs Fine-grain Call-by-value

It seems to me that Fine-grain call-by-value already subsumes CBV and CBN, using lambdas as thunks. What does CBPV improve upon FG-CBV or in what way is it "better"?
2
votes
1answer
77 views

Proving Progress for STLC with Linear and Unrestricted Types

In this paper Walker presents an extension of STLC with linear and unrestricted types. The proof of type soundness is left as an exercise to the reader. I encountered difficulty when attempting to ...
3
votes
0answers
81 views

CFG for $\lambda$-calculus with minimal parentheses

The typical presentation of the syntax of the $\lambda$-calculus is as an ambiguous CFG (or BNF) like the following: $$T \rightarrow \lambda X . T \mid T ~ T \mid X \mid (T)$$ Where we permit $X$ to ...
4
votes
1answer
68 views

if an argument of a lambda only passes itself if it is further evaluated, is runtime always finite?

In order for a lambda expression to run forever, there must be at least one lambda in the expression in which an argument is passed to itself. For example the following runs forever. $$ (\lambda x.xx)...
2
votes
2answers
180 views

Confusion about the definition of de Bruijn terms in the TAPL book

I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the ...
2
votes
1answer
90 views

Why is abstraction in lambda calculus called abstraction?

The term abstraction as I understand it, is used in many different contexts, but has one essential meaning, namely that it refers to the “general properties of some class of objects that doesn’t rely ...
3
votes
2answers
98 views

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed: let $f =\lambda x.x$ in $f f$ Obviously the $f$ is the identity function, so it's the same as let $id =\lambda x.x$ in $id$ $id$ I ...
2
votes
0answers
21 views

Understanding First conversion rules from church's lambda bible

While going through Church's text on Lambda calculus , I cam across the first set of conversion rules . Before writing out my query I would like to put the notation that church has used for ...
0
votes
0answers
33 views

how to build logical representation from dependency tree

I'm trying to build logical representation from dependency tree with python. i created the tree with stanford parser. How can I derive logical presentation from it using Lambda-calculus?
2
votes
0answers
50 views

Term for weak head normal forms that cannot be reduced in any environment

In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (...
1
vote
2answers
209 views

Application of lambda function in Simply Typed Lambda Calculus

I'm just getting started with STLC (Simply Typed Lambda Calculus) and I'm trying to understand an evaluation rule I've been given in some lecture notes by my professor. What it says is the following: ...
6
votes
1answer
115 views

How to model conditionals with first-class functions?

Since languages with recursible first-class functions are Turing-complete, they should be able to express anything expressible in any other programming language. Therefore, it should be possible to ...
1
vote
2answers
71 views

Term rewrite system for terms of lambda calculus?

Are there term rewrite systems, that can rewrite complex lambda term (with nested function application) into some other lambda terms, I.e. reorde function application and, possibly, introduce new ...
3
votes
0answers
33 views

Expressing definite clauses (Horn rules, logic programming) in lambda terms?

There is paper which expresses lambda terms in the terms of logic programming http://www.cse.unt.edu/~tarau/teaching/PL/docs/dbx.pdf Is there conversion in the other direction - expressing definite ...
7
votes
0answers
114 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
2
votes
1answer
55 views

Trying to verify the solution to a lambda calculus equation

I am going through the following introduction to lambda calculus : http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf At page 12 , the following has been asked to prove $ \...
2
votes
1answer
98 views

Reduction of the Y combinator

The Y combinator expression is as follows: $$ Y \equiv \lambda f .(\lambda x .f(xx) )) .(\lambda x .f(xx) ) $$ Now , if I am not wrong , then this expression can be reduced by seeing this as the ...
1
vote
0answers
24 views

confusion due to the apparent difference in semantics of two beta reductions

Let us consider the following lambda expression : $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ so $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ can be seen as $ (\...
2
votes
1answer
58 views

Rigorous reason against the seemingly wrong way of substitution

Let us consider the lambda calculus expression . $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ Now $\lambda x.x$ is seen as an argument . How to decide which bound variable should the ...
3
votes
1answer
89 views

Understanding Applicative Evaluation Order with the Z-Combinator

I am trying to understand how the Z-combinator (Y-combinator for applicative order languages) definition came about. As Python is applicative I am using Python for this. So I know Python's evaluation ...
2
votes
1answer
35 views

An explanation for Barendregt use of Y combinator in an equation

I am going through the following lecture notes on lambda calculus by Barendregt and Barendsen : http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf Here at page 12 , after ...
2
votes
1answer
54 views

Doing beta reduction while constructing the boolean expression in lambda calculus

I am going through beta reduction in lambda calculus . And beta reduction to my understanding is an act of substitution like in the following : $ (\lambda x.P) M $ is said to be beta reduced to : $...
6
votes
2answers
342 views

$\lambda$-calculus, is there encoding of for or while?

In $\lambda$-calculus, we can encode arithmetic, numbers, booleans, and even compute factorials of numbers, as shown here. Is there encoding of "for" or "while"?
2
votes
1answer
57 views

How is this lamda function beeing executed in an example for the Y combinator

I have spent a few hours now trying to understand how the Y Combinator is working and how it allows us to construct recursive functions with higher order functions. I have been going through this ...
4
votes
1answer
146 views

Some points about type checking of simply typed $\lambda$-calculus?

type checking I was preparing examples of type checking in simply typed $\lambda$-calculus. I wanted to explain it to my audience in the way of implementation. And I found a bit tricky point in the ...
3
votes
1answer
98 views

Abstractions in call-by-push-value

In "Call-by-push-value: A subsuming paradigm." (Levy, Paul Blain. Springer, Dordrecht, 2003. 27-47) terms of the lambda calculus get split in to values and computations, with the slogan "A value is, a ...
4
votes
2answers
65 views

Composition of handler types in algebraic effects and handlers

In the paper "An introduction to algebraic effects and handlers" (Pretnar, Matija. Electronic Notes in Theoretical Computer Science 319 (2015): 19-35), handlers get a handler type that looks like a ...
1
vote
1answer
63 views

It is possible to write any program (i.e. Turing complete) with just one single expression?

So I'm currently taking discrete math II at my university and I came across a somewhat philosophical question (so I apologize if this is question is hard to answer precisely) of whether mathematicians ...
4
votes
1answer
425 views

How do I arrive at the multiplication function in lambda calculus?

I'm familiar with how Church numerals are defined in the lambda calculus, i.e. as functions that take two arguments and apply the first argument $n$ times to the second. Then I have the successor and ...
2
votes
1answer
121 views

explaining $\lambda$-calculus/functional programming to someone used to Turing machines/procedural programming?

I have the following background: I have experience with object-oriented programming languages I find Turing machines and the concept of a "procedure" very intuitive. Yet I'm interested to ...
7
votes
2answers
104 views

Ackerman hierarchy for higher order primitive recursion in System T

Gödel defines in his System T primitive recursion over higher types. I found notes from Girard where he explains the implementation of System T on top of simply typed lambda calculus. On page 50 he ...