λ-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

5
votes
2answers
71 views

Is there an equivalent of lambda calculus for object oriented languages? [duplicate]

Lambda calculus serves as a foundation for all sorts of functional languages and its various extensions are compiler targets for languages like Haskell, ML, etc. So what is the equivalent for object ...
3
votes
2answers
136 views

Free and bound variables

I am familiar with free and bound variables theory , but while learning I somewhere saw this lambda expression ((lambda var ((fn1 var) & (fn2 var))) argument) From what I have learned it ...
-1
votes
1answer
83 views

Encoding of integer arithmetic counting using Lambda calculus [duplicate]

Does anyone know a way of showing an encoding of integer arithmetic counting using Lambda Calculus? Any references related to this would be much appreciated.
1
vote
0answers
21 views

How to get from factorial to a y-combinator?

In one of his conference talks Jim Weirich derives the applicative form of the y-combinator by refactoring a partial definition of factorial. The starting point in his talk is different than what ...
1
vote
1answer
26 views

Difference between a lambda term and a lambda expression

Is there any difference between a $\lambda$-term and a $\lambda$-expression? Looking at the recursive definitions on Wikipedia of $\lambda$-term and $\lambda$-expression, they are equivalent. But I ...
1
vote
0answers
26 views

Expressions that cannot be evaluated in normal-order?

It seems to me that when the outermost|toplevel function is itself an expression to be evaluated (i.e.: a higher-order function returning the function to be applied at top-level), then normal-order ...
2
votes
0answers
39 views

How does this addition for Church numerals work with Y combinator?

I am currently preparing for an exam. In one of the old exams, you have to create a $\lambda$ expression $add$ that can add two church numerals. But the church numerals are not the usual ones, but ...
1
vote
0answers
18 views

How to reduce this with all 4 of normal applicative by-name by-value?

Given mult = \x -> \y -> x*y I am trying to reduce (mult (1+2)) (2+3) with each of the strategies: normal-order ...
0
votes
1answer
20 views

Can the lambda functions in Church numbers be swapped?

I've learned that one can represent natural numbers with lambda calculus like this: \begin{align*} c_0 &= \lambda s. \lambda z. z\\ c_1 &= \lambda s. \lambda z. s~z\\ c_2 &= \lambda s. ...
2
votes
0answers
25 views

How do stable functions 1 => 1 relate to Bool?

One way to interpret the (simply typed) lambda calculus is via coherence spaces (Proofs and Types, chapter 8). For example, we can consider the space containing token element ($\mathbf{1}$) and the ...
2
votes
1answer
46 views

Smallest non-halting unlambda program

Is ```sii``sii the smallest Unlambda program that doesn't halt? In other words, what is the smallest non-terminating combinator term in SKI augmented with $C$ ...
5
votes
0answers
42 views

Bounded existential polymorphism

In Pierce's "Types and Programing Languages" he, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
5
votes
1answer
56 views

What is $Prop$ in the calculus of constructions?

I'm looking at the Calculus of Constructions and its place in the Lambda Cube. If I understand correctly, each axis of the cube can be thought of as adding another operation involving types to the ...
3
votes
1answer
59 views

Meaning of type inference rule for abstraction in lambda-calculus

Below is a snippet about simply typed lambda-calculus from CS152: Programming Languages Lecture 9 | Simply Typed Lambda Calculus, on printed‑page 15, indexed 23. $$ \frac {\Gamma, x: \tau_1 \vdash e: ...
7
votes
2answers
120 views

Combinatory interpretation of lambda calculus

According to Peter Selinger, The Lambda Calculus is Algebraic (PDF). Early in this article he says: The combinatory interpretation of the lambda calculus is known to be imperfect, because it ...
1
vote
2answers
72 views

Call‑by‑name will succeeds where call‑by‑value may fails: some example cases?

I've landed to SML pages, comparing call‑by‑name and call‑by‑value, asserting the former always succeed while the latter may fails. As this seems counter intuitive to me, I feel at least an example ...
1
vote
1answer
47 views

No need to rename a free variable in substitution?

I wonder if the following two substitutions are correct: $$(x\,y)[x:=y] = (y\,y)$$ $$ \lambda y. (x\,y) [x:=y] = \lambda z.(y\,z)$$ They are what I understand from ...
1
vote
1answer
83 views

recursive lambda expressions

From http://www.seas.gwu.edu/~rhyspj/spring09cs145/lab8/lab82.html The lambda operator does not bind every occurrence of its variable because "shadowing" can occur. A variable is bound by its ...
1
vote
2answers
154 views

What are the axioms, inference rules, and (formal) semantics of lambda calculus?

Wikipedia says that lambda calculus is a formal system. It defines lambda calculus by giving its alphabet, and inductively describing what is inside its formal language. Since lambda calculus is a ...
2
votes
0answers
123 views

Prove that turing machines and the lambda calculus are equivalent

It is known that a turing machine and the lambda calculus are equivalent in power. I now want to try to prove this myself. I think proving that the lambda calculus is at least as powerful as a turing ...
3
votes
2answers
95 views

Composition of combinators with arities greater than one

In combinatory logic, the axiom of composibility asserts that for any two combinators, $A$ and $B$, there exists a combinator $C$ that composes $A$ and $B$. That is, for all $A,B,x$ there exists a ...
3
votes
0answers
92 views

Is there any programming system that enables reversible computations?

Better explained with examples, I need a programming system with the following characteristics: ...
5
votes
1answer
114 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 ...
3
votes
0answers
44 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
202 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
98 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
65 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
119 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
34 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 ...
12
votes
4answers
268 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'. In this lecture, he introduces the concept of Y-combinators, which essentially finds the fixed point for ...
2
votes
2answers
66 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
20 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
140 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 ...
7
votes
3answers
236 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
221 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
83 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
80 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
43 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 ...
7
votes
1answer
149 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
48 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
174 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
87 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
89 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 ...
3
votes
1answer
154 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
99 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
36 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
154 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
163 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
50 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
102 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 ...