The tag has no wiki summary.

learn more… | top users | synonyms

1
vote
1answer
78 views

What can be proven within Simply Typed lambda calculus?

I was reading http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus and I'm having a hard time thinking of anything remotely interesting that can be proven within Simply Typed lambda calculus. Am ...
0
votes
2answers
49 views

Induction on the length of a $\lambda$-term

I'm a bit confused about a statement that I see often in the $\lambda$-calculus literature. Namely, what exactly does the following statement mean: "By induction on the length of $M\in\Lambda$." ? In ...
0
votes
1answer
94 views

$\alpha$-equivalence and the substititution operation over equivalence classes

This post is divided in two parts, viz. Definitions and Question. Definitons The following definitions are adapted from Lecture notes on the Curry-Howard Isomorphism (by Sorensen and Urzyczyn), ...
3
votes
1answer
79 views

What's the intuition behind this definition of ordered pair in the $\lambda$-calculus?

On this page, we have the following definitions. pair = λabf.fab first = λp.p(λab.a) second = λp.p(λab.b) So I tried computing "first (pair a b)," and sure ...
2
votes
1answer
63 views

Is the empty string a valid lambda expression?

My first intuition is yes, because the empty string is usually a valid instance of whatever object. There's usually good conceptual reasons for this. But in lambda calculus, I believe the standard ...
8
votes
4answers
369 views

How do lambda calculus most basic definitions work?

Good afternoon, I'm trying to learn lambda calculus, and I do understand the notation (it's not hard, $f=\lambda a_1.\cdots\lambda a_n.x=\lambda a_1\cdots a_n.x\Leftrightarrow f(a_1;\cdots;a_n)=x$), ...
0
votes
1answer
102 views

Which way of writing functions is the most correct?

In functional programming it's not uncommon to bind a closure/lambda/anonymous function to a value name, i.e. $$f = x \mapsto x^2 + 3$$ so I've been wondering which is more right to do in ...
3
votes
0answers
140 views

Is there an algorithm to separate lambda calculus terms using Böhm's theorem?

Böhm's theorem says that given lambda terms $r$ and $s$ with non-equivalent normal forms, there exists $\vec{a}$ terms such that $r\vec{a}=t$ and $s\vec{a}=f$. I'm finding it hard to determine what ...
0
votes
1answer
62 views

What is the result of (λx.λy.x + ( λx.x+1) (x+y)) ( λz.z-4 5) 10?

Could you explain what should I do about λx.λy.x part? Thanks.
3
votes
3answers
206 views

Book on lambda calculus logic and type theory

Can someone recommend me a book for self study which will cover topics of logic, lambda calculus and type theory. I know about "Computability and Logic" written by Bolos but it describe recursive ...
2
votes
1answer
65 views

How the the Identity in Church Numerals not the 'succ' function (ie. x + 1)

I realize this is probably a simple question for most people, but it is something that I am just having a hard time understanding. The numbers 1 and 2 is defined as: $1 = \lambda f. \lambda x. ...
0
votes
1answer
81 views

evaluate the lambda expression call by value

$(\lambda x.\lambda y.(\lambda x.yx)xy)(\lambda y.y)(\lambda x.x(\lambda y.y))$ I know in $(\lambda x.M)N$, if M has bound variables same as free variables in N, we rename the bound variables. IN ...
0
votes
1answer
116 views

Identifying All Redexes in Lambda Expression

I am self-studying Lambda calculus and have encountered a question where I need to identify all the redexes of the following expression: ...
0
votes
1answer
71 views

Lambda Calculus Expression Evaluation

I am looking at the following lambda calculus expression: (λx.(λy.(x(λx.xy))))y. Could somebody help me to evaluate it? I am guessing that the first step would be ...
2
votes
1answer
151 views

A problem with lambda calculus notation and semantics for function-valued functions

I would like to understand how to use the $\lambda$-notation to write usual (set-theoretic) functions, and if it is possible at all. Here are my naïve attempts. Assume that all variables are ...
0
votes
1answer
55 views

Adding Parentheses to Lambda Expression

I'm new to lambda calculus and was wondering if transforming the lambda expression $v\lambda v.v$ into $v(\lambda v.)v$ produces the same expression. Could someone help out?
0
votes
1answer
87 views

Is it appropriate to do alpha reduction before substitution?

In the lambda expression (λx. (λy. y z)(λw. w) z x)[z→y], I'm inclined to change y to another variable, then perform the substitution. Is this the correct way to approach this ...
3
votes
1answer
97 views

Lambda Calculus Equivalence

I'm a bit new to lambda calculus and was wondering about the equivalence of two expressions $$(\lambda x.\lambda y.xy)\lambda z.z\overset{?}=(\lambda x.\lambda y.xy)(\lambda z.z)$$ Can anyone help ...
1
vote
1answer
42 views

Universal quantification via lambda binding?

I remember once saw somewhere that a universally quantified formula can be written using $\lambda$. But I cannot recall very clearly. I have an vague impression that is is something of the form: ...
0
votes
1answer
54 views

$\mid$ in simply typed lambda calculus

$e = x \mid \lambda x\!:\!\tau.e \mid e \, e \mid c$ So, what is $\mid$ in this example of simply typed lambda calculus? The syntax of the simply typed lambda calculus is essentially that ...
1
vote
1answer
90 views

Applying substitutions in lambda calculus

For computing $2+3$, the lambda calculus goes the following: $(\lambda sz.s(sz))(\lambda wyx.y(wyx))(\lambda uv.u(u(uv)))$ I am having a hard time substituing and reaching the final form of $(\lambda ...
4
votes
2answers
132 views

How does second-order logic relate to lambda calculus?

How does second-order arithmetic/logic relate to lambda calculus? By lambda calculus, I mean both typed and untyped. And is there any relationship with recursive and recursively enumerable sets? ...
1
vote
1answer
50 views

How does lambda calculus explain relation between the name and the value?

In some textbook I have met a statement, that discovery of lambda calculus explained the relation between name and value. How it did this in a simple example? UPDATE I don't remember the context, ...
1
vote
2answers
162 views

Recursive relation using successor function

What is the recursive relation for $$H(m)=2^{(m^2)}$$ using successor function recursive relation for multiplication: $$mult(x,0)=0; mult(x,S(y))=add(x,mult(x,y))$$ recursive relation for addition: ...
-1
votes
1answer
178 views

Evaluating lambda expression

$((λfx.f(f(x))) (λy.y^2)$ (1) is finally evaluated to $1^4=1$ $(3)(3) (\text{inc})(0)=(27)(\text{inc})(0)=27$ Is λfx the same as λf.λx That is is $((λfx.f(f(x))) (λy.y^2) equivalent to ...
1
vote
1answer
76 views

Recursive functions, successor function

How to show that the power function $\displaystyle A=2^{m^2}$ is primitive recursive based on successor function? Thanks much in advance!!!
0
votes
1answer
72 views

$\lambda$-calculus: structural induction principle over $\Lambda$

The set $\Lambda$ is given inductively by: $x\in\Lambda$, if $x$ is a variable; $(\lambda x M)$, if $x$ is a variable and $M\in\Lambda$; $(MN)$, if both $M,N\in\Lambda$. Now, consider the ...
2
votes
1answer
132 views

Cartesian closed categories with double negation elimination

Let $\mathcal{C}$ be a cartesian closed category with an initial object. The following facts are well known: The initial object of $\mathcal{C}$ is strict: any morphism $X \to 0$ is necessarily an ...
1
vote
2answers
292 views

Substitution in lambda calculus

I have just started reading lambda calculus. In substitution it says $(\lambda x.M)N= [N/x]M$ (means all the free occurrences of $x$ in $M$ will be substituted by $N$) But $x$ is a bound variable. ...
1
vote
1answer
82 views

What are the differences between these two Lambda expressions?

What are the diffs between these two? $$\lambda x.((\lambda x.x)x)$$ $$(\lambda x.(\lambda x.x))x$$ and why? My understanding is that: ...
2
votes
1answer
169 views

Evaluate expressions in lambda calculus

Consider $(\;(\lambda f.\lambda x. f(f(f(x))))\;(\lambda g.\lambda y.g(g(y))) \;)$. Lets take the first lambda function, now $(\lambda f.\lambda x. f(f(f(x))))\;(\lambda x.x+1)(0) = 3 $ right? And ...
4
votes
0answers
315 views

Krivine Machine

Can someone please point out online resources to learn about Krivine Machine? My professor briefly touched it while teaching a course in Computer logic. google did not turn up much except some papers ...
2
votes
1answer
257 views

How come Lambda Calculus is a calculus? [duplicate]

Possible Duplicate: What do Algebra and Calculus mean? Where are the numbers? derivatives? integrals? limits? If I understand it correctly, lambda calculus is all about symbols. There are ...
0
votes
0answers
65 views

Inconsistencies in a set of conditions

I am looking for algorithms to find inconsistencies in a set of IF-THEN-ELSE conditions. I am aware of lambda calculus as a model to represent these. Are there any other models? Example Then rules ...
0
votes
1answer
85 views

Proving combinator identity KMN=M

Have a problem proving K MN=M By the K combinator definition $ (\lambda x y.x) M N $ Parenthesized $ ((\lambda x. (\lambda y.x)) M) N $ By the principal axiom of lambda calculus $ (\lambda y.M) N ...
0
votes
0answers
106 views

What binary operation lambda quantifier corresponds to?

Observation: Sigma summation is iterative form of binary plus. Pi-capital product is iterative form of multiplication. Lattice supremum is iterative form binary meet. Lattice infinum is iterative ...
11
votes
1answer
633 views

If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?

There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily ...
3
votes
2answers
204 views

What is the shortest function of lambda calculus that generates all functions of lambda calculus?

I suspect there's a good chance the answer to this is unknown and hard (or at least extremely tedious), but I figured it would be worth asking. It's well known that the functions $K:=\lambda ...
0
votes
1answer
633 views

Expressions: What is a “sub-expression?”

Again, I'm trying to understand Martin Henson's "Elements of Functional Languages." He talks about "maximal free expression." For example, M of EXP is a maximal free expression of N of EXP iff M is ...
0
votes
2answers
889 views

Lambda Calc: bound and free variables?

I'm trying to work through "Elements of Functional Languages" by Martin Henson. On p. 17 he says: $v$ occurs free in $v$, $(\lambda v.v)v$, $vw$ and $(\lambda w.v)$ but not in $\lambda v.v$ or in ...
6
votes
2answers
412 views

Is this formula really the nine axioms?

I was reading a note from guardian.uk called What lurks beneath a scientist's lab coat?, a little gallery of geeky-tattoos. However, number 11 in the series has the following image and caption text: ...
0
votes
1answer
82 views

implementation of xnor with lambda

i dont know how to ask my question but here it is... i have implementation of "NOT" and "True" and "false",but if i want to have "xnor" according to the example beneath: (true) T--->λx.λy.x (false) ...
0
votes
1answer
390 views

Looping (ω) Combinator

Can someone explain this combinator? I understand $\lambda x. x$, but I don't understand $\lambda x. x x$ From what I've gathered, this means given x, return the application of x to x. I don't ...
-1
votes
2answers
179 views

how to show two expressions have the same $\beta-\eta$ normal form

======================= Original Post ====================== In lambda calculus, we define the boolean operators as below: $$ AND \to \lambda{}pq.pq\boldsymbol{F} \to ...
2
votes
1answer
210 views

Where to find $\lambda$-calculus examples? For instance, how to check if a list is empty?

I'm trying to remove many layers of dust from my knowledge about $\lambda$-calculus, without my notes from classes (several hundreds of km and 5 years away). I was trying to understand the examples ...
5
votes
2answers
1k views

What's the point of eta-conversion in lambda calculus?

I think I'm not understanding it, but eta-conversion looks to me as a beta-conversion that does nothing, a special case of beta-conversion where the result is just the term in the lambda abstraction ...
18
votes
2answers
1k views

Why is lambda calculus named after that specific Greek letter? Why not “rho calculus”, for example?

Where does the choice of the Greek letter $\lambda$ in the name of “lambda calculus” come from? Why isn't it, for example, “rho calculus”?
1
vote
1answer
103 views

Understanding recursion in λ calculus

In recursion for λ calculus, I was wondering why the following two are equal (λx.g (x x)) (λx.g (x x)) g ((λx.g (x x)) (λx.g (x x))) How shall I understand g ((λx.g (x x)) (λx.g (x x)))? ...
7
votes
2answers
1k views

Can someone explain the Y Combinator?

The Y combinator is a concept in functional programming, borrowed from the lambda calculus. It is a fixed-point combinator. A fixed point combinator $G$ is a higher-order function (a functional, in ...
2
votes
1answer
489 views

Use of parenthesis in lambda calculus

As a summer project I am trying to learn lambda calculus. I am not that good with math but I have learned myself several programming languages and somehow got the idea that learning lambda calculus ...