Questions tagged [lambda-calculus]

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

Filter by
Sorted by
Tagged with
3
votes
2answers
113 views

How to decide the scope of the following lambda expression?

I am having a difficulty in deciding the scope of the left-most lambda in the following expression. λx.x(λuv.v)(λab.a)(λcd.c) I have learnt that we should put ...
0
votes
1answer
125 views

What is a preterm parser?

I am working with HOL-Light parser and keeping seeing references to preterm parser. What is a preterm parser? The most informative statement I find is from the HOL-Light reference for the ...
1
vote
1answer
1k views

Normal form Lambda calculus expression

I need a little help with a lambda calculus reduction to normal form: $$(\lambda xxxx.xx)(\lambda x.xx)(\lambda x.x)y((\lambda x.x)x)$$ It should be solved like this: $$xx(\lambda x.x)y((\lambda x.x)x)...
7
votes
2answers
279 views

Is there an always-halting, limited model of computation accepting $R$ but not $RE$?

So, I know that the halting problem is undecidable for Turing machines. The trick is that TMs can decide recursive languages, and can accept Recursively Enumerable (RE) languages. I'm wondering, is ...
10
votes
2answers
1k views

What makes lambda calculus relevant to study?

I'm starting an undergraduate computer science course next fall, but I can't really understand λ-calculus in the context of functional programming. I may be misinterpreting this completely, but based ...
4
votes
1answer
772 views

Are there a lambda-mu expression equivalent to the yin yang puzzle?

The yin yang puzzle was written in Scheme. Since it uses call/cc, it is not possible to express it in a pure lambda expression, unless we do a CPS transform. However, given the fact that $\lambda \mu$...
0
votes
1answer
211 views

Free and bound variables in a lambda-calculus term

For this term: $\lambda x.(f (g x))$, what are the free and bound variables? I'm confused as to how to expand this so it will be easier to see. If I expand this will it be $\lambda x. \lambda f....
2
votes
1answer
817 views

A program that cannot be written in (simply-)typed lambda calculus but only in lambda calculus or Turing-complete language

Programmers do sometimes write a program that creates infinite loop if some particular input is passed into the program. But Simply-typed lambda calculus has to stop - so the question is, can anyone ...
7
votes
1answer
253 views

Free and Bound in Lambda Calculus

Here's something from Slonneger's "Syntax and Semantics of Programming Languages": A variable may occur both bound and free in the same lambda expression: for example, in λx.yλy.yx the first ...
4
votes
1answer
137 views

Substitution by structural recursion

Following the article's notation, I write $\mathcal{F}$ for the category of presheaves on a (suitable) category $\mathbb{F}$, $TV$ for the presheaf of terms, $\delta$ for the context extension, and $\...
10
votes
3answers
611 views

anonymous lambda functions (functional programming)

What are anonymous (lambda) functions? What is the formal definition of an anonymous function in a functional programming language? In my simple terms, when I am programming in scheme/lisp I would ...
30
votes
4answers
5k views

Clear, intuitive derivation of the fixed-point combinator (Y combinator)?

The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as: FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. ...
3
votes
0answers
617 views

λ-Calculus extensions: meaning of extension symbols

When working with λ-Calculus I see lots of extensions that use other symbols such as ∀ <:Top {} ←, which are from "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce. ...
6
votes
0answers
429 views

Test cases for λ-Calculus

For testing automated theorem provers we have Seventy-Five Problems for Testing Automatic Theorem Provers by Pelletier. Are there any such standard/well regarded tests for a λ-calculus that verify ...
14
votes
2answers
12k views

“Applicative order” and “Normal order” in lambda-calculus

Applicative order: Always fully evaluate the arguments of a function before evaluating the function itself , like - $(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x. x^2(2+1))\...
12
votes
4answers
4k views

Can someone give a simple but non-toy example of a context-sensitive grammar?

I'm trying to understand context-sensitive grammars. I understand why languages like $\{ww \mid w \in A^*\}$ $\{a^n b^n c^n \mid n\in\mathbb{N}\}$ are not context free, but what I'd like ...
16
votes
3answers
606 views

Studying Programming Language Theory

I have recently become extremely interested in understanding and proving aspects of (functional) programming languages. However as I dive deeper in, things like $\lambda$ calculus, category theory, ...
6
votes
1answer
211 views

Showing the function=? is impossible

Here's a lab from a first-year computer science course, taught in Scheme: https://www.student.cs.uwaterloo.ca/~cs135/assns/a07/a07.pdf At the end of the lab, it basically presents the halting problem,...
21
votes
5answers
1k views

Lambda calculus outside functional programming?

I'm a university student, and we're currently studying Lambda Calculus. However, I still have a hard time understanding exactly why this is useful for me. I realize if you do loads of functional ...
3
votes
1answer
128 views

Are two terms where one is without a $\lambda\beta$ normal form unconvertible in $\lambda\beta$?

I know that if you try and make the theory $$\lambda\beta+\{s = t\ |\text{ s, t are terms without }\lambda\beta\text{ normal forms}\}$$ then that theory becomes inconsistent. Are two terms where one ...
11
votes
1answer
2k views

Concise example of exponential cost of ML type inference

It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
8
votes
2answers
2k views

Lambda Calculus simplification

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. $$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda sz.sz)$$...
5
votes
1answer
317 views

Free variables of (λx.xy)x and bound variables of λxy.x

I was solving exercises on Lambda calculus. However, my solutions are different from the answers and I cannot see what is wrong. Find free variables of $(\lambda x.xy)x$. My workings: $FV((\lambda x....
23
votes
5answers
1k views

$\lambda$-calculus with reflection

I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs. Is there an untyped $\lambda$-calculus extension that ...
32
votes
1answer
2k views

Does there exist a Turing complete typed lambda calculus?

Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?
14
votes
2answers
5k views

Representing Negative and Complex Numbers Using Lambda Calculus

Most tutorials on Lambda Calculus provide example where Positive Integers and Booleans can be represented by Functions. What about -1 and i?
13
votes
2answers
674 views

Do Higher Order Functions provide more power to Functional Programming?

I've asked a similar question on cstheory.SE. According to this answer on Stackoverflow there is an algorithm that on a non-lazy pure functional programming language has an $\Omega(n \log n)$ ...
8
votes
3answers
426 views

Simple explanation as to why certain computable functions cannot be represented by a typed term?

Reading the paper An Introduction to the Lambda Calculus, I came across a paragraph I didn't really understand, on page 34 (my italics): Within each of the two paradigms there are several versions ...
26
votes
1answer
1k views

Is there a typed SKI calculus?

Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the ...
7
votes
1answer
279 views

Why are lambda-abstractions the only terms that are values in the untyped lambda calculus?

I am confused about the following claim: "The only values in the untyped lambda calculus are lambda-abstractions". Why are the other terms not values? What does it mean for a lambda-abstraction to be ...
7
votes
1answer
271 views

Reduction rule for IF?

I'm working through Simon Peyton Jones' "The Implementation of Functional Programming Languages" and on page 20 I see: IF TRUE ((λp.p) 3) ↔ IF TRUE 3 (per β red) (1) ...
6
votes
1answer
3k views

Lambda Calculus beta reduction

I am trying to learn Lambda calculus from here and while trying to solve some problems, I got stuck. I was trying to solve the following problem (page 14, excercise 2.6 part (i): Simplify $M \equiv (...
10
votes
1answer
521 views

A lambda calculus evaluation involving Church numerals

I understand that a Church numeral $c_n$ looks like $\lambda s. \lambda z. s$ (... n times ...) $s\;z$. This means nothing more than "the function $s$ applied $n$ times to the function $z$". A ...
8
votes
1answer
289 views

Lambda Calculus Evaluation

I know this is a simple question but can someone show me how $(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduces to $\lambda x. \lambda y. y$.
36
votes
2answers
2k views

Quantum lambda calculus

Classically, there are 3 popular ways to think about computation: Turing machine, circuits, and lambda-calculus (I use this as a catch all for most functional views). All 3 have been fruitful ways to ...
11
votes
3answers
763 views

Is there a difference between $\lambda xy.xy$ and $\lambda x.\lambda y.xy$?

I am currently learning the lambda calculus and was wondering about the following two different kinds of writing a lambda term. $\lambda xy.xy$ $\lambda x.\lambda y.xy$ Is there any difference in ...
21
votes
2answers
2k views

What is beta equivalence?

In the script I am currently reading on the lambda calculus, beta equivalence is defined as this: The $\beta$-equivalence $\equiv_\beta$ is the smallest equivalence that contains $\rightarrow_\beta$...
29
votes
2answers
639 views

Characterization of lambda-terms that have union types

Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping): $$ \dfrac{\...

1
5 6 7 8
9