λ-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
38 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
35 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
48 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
51 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
105 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
58 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
26 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
74 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
118 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
77 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
81 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
85 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
108 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
40 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
95 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
46 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
57 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
98 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
32 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 ...
11
votes
4answers
240 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
63 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
19 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
126 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 ...
6
votes
3answers
184 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
181 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
74 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
38 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
129 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
40 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
110 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
79 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
85 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
145 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
82 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
30 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
144 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
156 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
93 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
128 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
140 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
132 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
181 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
210 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
111 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
166 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
90 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
51 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
320 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 ...