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

learn more… | top users | synonyms

2
votes
1answer
72 views

What does Tarski's Fixed-Point theorem give us that that Y-Combinator does't

I'm taking a graduate course on the theory of functional programming, based on Paul Taylor's "Practical Foundations of Mathematics." I understand the statement of Tarski's theorem about how for any ...
2
votes
0answers
33 views

Does there exist a type system for a non-let-polymorphic lambda calculus?

I'm wondering if there is a way to extend Hinley-Milner's type system to allow polymorphic types without the need of a let construct, by adding an intersection type (as Dan pointed out) that ...
3
votes
1answer
66 views

Lambda Calculus: How do evaluation contexts “work”

In the pure lambda calculus, we have the inductively defined set of terms (the grammar): $$e::= x \mid \lambda x . e \mid e_1 e_2$$ Under the call-by-value evaluation strategy, we have the inference ...
1
vote
1answer
25 views

Abstract Syntax Tree of Pure Lambda Calculus

I was wondering if anyone had any good references or book recommendations that cover abstract syntax trees (ASTs). Specifically, I am interested in the abstract syntax trees of different evaluation ...
0
votes
2answers
32 views

Role of Term Constants in Simply Typed Lambda Calculus

In the Wikipedia article on Simply Typed Lambda Calculus (among other places), there is a notion of a "term constant". This is particularly notable in the production grammar given: In this ...
6
votes
2answers
72 views

Lambda calculus: difference between contexts and evaluation contexts

Firstly, I'd like to say that my text below may contain errors, so feel free to point out any mistakes in my formulation of the question. Consider an untyped lambda calculus with booleans and ...
0
votes
1answer
26 views

Verify the type of a lambda expression

I need to verify the type for the lambda expression: $\lambda f.\lambda x.f (f x)$ My method gives me: $(a\rightarrow c)\rightarrow b\rightarrow c$ Im trying to define it in Haskell (on Hugs) like ...
9
votes
4answers
187 views

Why is it important for functions to be anonymous in lambda calculus?

I was watching the lecture by Jim Weirich, titled 'Adventures in Functional Programming' (http://vimeo.com/45140590). In this lecture, he introduces the concept of Y-combinators, which essentially ...
2
votes
2answers
55 views

How should $\lambda x. \lambda y. f z x y \stackrel{\eta}{=} \lambda x. f z x$ be read?

I'm currently learning untyped $\lambda$-calculus and especially the $\eta$-reduction. The professor hat the following in his slides: $$\lambda x. \lambda y. f~z~x~y \stackrel{\eta}{=} \lambda x. ...
1
vote
0answers
18 views

Definition of zero checking expression [closed]

Let $T\equiv\lambda xy.x$ $F\equiv\lambda xy.y$ Numbers are represented as: $0\equiv\lambda sz.z$ $1\equiv\lambda sz.s(z)$ $2\equiv\lambda sz.s(s(z))$ $N\equiv\lambda sz.\underbrace{s(s( ... ...
2
votes
1answer
115 views

Lazy lists with call-by-value reduction strategy

I am currently writing lists with lazy semantics in the pure lambda-calculus with call-by-value reduction strategy. Here is an example: http://pastebin.com/yLtjdDzV Here is a simple (and very ...
4
votes
2answers
105 views

A quine in pure lambda calculus

I would like an example of a quine in pure lambda calculus. I was quite surprised that I couldn't find one by googling. The quine page lists quines for many "real" languages, but not for lambda ...
6
votes
2answers
140 views

Define a list using only the Hindley-Milner type system

I'm working on a small lambda calculus compiler that has a working Hindley-Milner type inference system and now also supports recursive let's (not in the linked code), which I understand should be ...
6
votes
2answers
77 views

How strong is equivalence of lambda expressions?

Consider two lambda expressions $\mu$, $\nu$ representing computable functions $f_{\mu,\nu}:\mathbb{N} \rightarrow \mathbb{N}$. If $\mu$ and $\nu$ are equivalent under the combination of ...
2
votes
0answers
65 views

Can type information be encoded in the untyped lambda calculus?

I'm going to take the few pieces of knowledge I have about lambda calculi and ask a pair of very uninformed questions :-) Is it possible to "embed" the corners of the lambda cube within the untyped ...
1
vote
1answer
36 views

Normal order sequencing vs applicative order sequencing

I'm trying to understand this lecture, section 2.7. Why would the normal order sequencing print out "hello" "world" and not ...
4
votes
1answer
93 views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about this algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the arguments will determine ...
5
votes
1answer
29 views

Simply Typed Combinatory Logic?

As there is an untyped lambda calculus, and a simply-typed lambda calculus (as described, for example, in Benjamin Pierce's book Types and Programming Languages), is there a simply-typed combinatory ...
1
vote
1answer
73 views

how to solve this lambda expression with free variable/s

Iam a beginner in Lambda Calculus, I have a expression saying (λx.xy) Here y is a free variable and x is a bound variable. My question is what would be the value of the expression (which has free ...
2
votes
1answer
62 views

Would adding recursive named functions to Simply typed lambda calculus make it Turing complete?

Say I have Simply typed lambda calculus, and add an assignment rule: <identifier> : <type> = <abstraction> Where ...
3
votes
1answer
81 views

What do functions look like, if I stated out with the categoical model of my type theory?

I see how objects in a category stand for types, but where do I find the terms and more specifically the rules which tell me which of them are allowed? When I e.g. consider a Cartesian closed category ...
2
votes
1answer
140 views

Is there a theory/abstraction behind OOP?

Functional programming has the very elegant Lambda Calculus and its variants as a backup theory. Is there such a thing for OOP? What is an abstraction for the object oriented model?
2
votes
1answer
65 views

Confused about beta-reduction/shifting in untyped $\lambda$-calculus with de Bruijn terms

In Types and Programming Languages, the family of sets of terms with de Bruijn indices in the untyped $\lambda$-calculus is defined in this way: Let $T$ be the smallest family of sets $\{T_0, T_1, ...
2
votes
1answer
29 views

Is this $\beta$-reduction well defined?

Would it be possible to apply $(\lambda x.\lambda y. x)$ to the argument $y$? It seems to me that this must not be possible as it would give a different answer if applied to a constant, call it ...
1
vote
1answer
116 views

How do you say when a language is Turing-complete only in a trivial way?

I didn't know how to ask this question before but now that I'm reading about typed lambda calculus I think I've got a better idea. There is this answer to a question asking whether CSS is Turing ...
5
votes
2answers
147 views

Equivalence of two lambda expressions for NOT

I've seen two different lambda expressions for the logical NOT function. One of them just applies its parameter to constants true and ...
0
votes
1answer
48 views

Which redexes are there in $\lambda s. \lambda z. (\lambda u. z)(\lambda v. v)$? How to substitute arguments?

I'm having difficulties understanding lambda calculus, specially identifying what's a redex. Which redexes are there in $\lambda s. \lambda z. (\lambda u. z)(\lambda v. v)$? The book uses $(\lambda ...
1
vote
1answer
88 views

What's wrong with my beta reduction of pred c_0 on Church numerals?

I'm trying to calculate $\text{pred}\, c_0$, where $\text{pred}$ is the previous church encoded number and $c_0$ is the number $0$ ($\lambda s. \lambda z. z$). The formula for $\text{pred}$ is ...
2
votes
1answer
114 views

What is the name of this combinator?

I've recently started casually reading into combinatorial logic, and I noticed that a higher-order function that I regularly use is a combinator. This combinator is actually pretty useful (you can use ...
3
votes
1answer
123 views

lambda calculus as a type theory

From the Introduction section of Homotopy Type Theory book: Type theory was originally invented by Bertrand Russell ... It was later developed as a rigorous formal system in its own right(under ...
3
votes
2answers
122 views

To what does typing correspond in a Turing Machine?

I hope my question makes sense: Starting with the premise that the untyped $\lambda $ calculus is equivalent in power to a Turing machine, to what in a Turing machine does adding types to the $\lambda ...
1
vote
1answer
170 views

Is lambda calculus suitable for expressing semantics of non-functional languages?

Would it be convenient to express semantics of imperative languages (e.g. C) and object-oriented languages (e.g. Java) with $\lambda$-calculus? Or in the other words: is $\lambda$-calculus a suitable ...
10
votes
2answers
201 views

Are there peer-reviewed papers studying the pros and cons of functional programming?

Can somebody refer me to peer-reviewed papers studying the advantages or disadvantages of writing code in a functional style? Are there papers which discuss the applications of Lambda Calculus in ...
1
vote
1answer
100 views

defining lambda expressions

I am studying for my exam and I wanted to do some extra excercises, but I have some problems with solving :) Can anyone please help or give me some advice where to start? Thank you! We can represent ...
2
votes
2answers
144 views

Can the Lambda Calculus or Turing Machines model signals, callbacks, sleep/wait, or buses?

I have a deep appreciation for formalisms like the Turing Machine and the $\lambda$-Calculus, and enjoy studying them and learning more about how they relate to physical computers. I am now learning ...
3
votes
2answers
86 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
47 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
262 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 ...
5
votes
2answers
115 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 ...
8
votes
2answers
327 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 ...
3
votes
1answer
123 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 ...
0
votes
1answer
71 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 ...
1
vote
1answer
192 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 ...
3
votes
1answer
57 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 ...
3
votes
1answer
79 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 ...
8
votes
3answers
259 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 ...
8
votes
2answers
565 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. ...
1
vote
0answers
240 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. ...
1
vote
0answers
145 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 ...
3
votes
2answers
879 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. ...