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

0
votes
0answers
33 views

LL(1) grammar for the untyped lambda-calculus

What I want to do I am trying to define a LL(1) grammar of the lambda-calculus. What I did Here is the grammar: $Term \to Abs$ $Term \to App$ $Abs \to \lambda \ id \ . \ Term$ $App \to Var \ ...
1
vote
1answer
28 views

Difference between normal-order and applicative-order evaluation

The language I'm learning is Scheme and I'm working on an exercise that gives this: ...
1
vote
0answers
8 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
0
votes
0answers
31 views

Lambda Calculus Reduction

I am a little confused to reduce these lambda calculus expressions. I am instructed to give applicative and normal order reductions for these expressions. $(a):$ $$(\lambda x. (\,(\lambda y.(* 2 ...
2
votes
1answer
37 views

Lambda Calculus Notation

I'm reading through the paper Transactors: A Programming Model for Maintaining Globally Consistent Distributed State in Unreliable Environments by John Field and ...
1
vote
0answers
52 views

Models of Computation and What they can model [closed]

Some days ago i've discovered that in most of what we call "models of computation ", we can possibly model tasks other than computation itself . For instance, in lambda calculus we can model control ...
5
votes
2answers
109 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
151 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
109 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
34 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
29 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
30 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
43 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
21 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
26 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
60 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
47 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
65 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
68 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: ...
10
votes
2answers
160 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
74 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
73 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
89 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
188 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
147 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
102 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
101 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
124 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 ...
4
votes
0answers
52 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
303 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
139 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
76 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
148 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
35 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
292 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
70 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
22 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
2answers
169 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. I tried to construct pleasant to use and relatively efficient "lazy" functions on ...
7
votes
3answers
265 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
300 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
85 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
84 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
46 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 ...
8
votes
1answer
204 views

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

I'm reading about the Hindley-Milner typing 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 ...
5
votes
1answer
60 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
204 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
113 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
90 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 ...
5
votes
2answers
233 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?