The lambda-calculus tag has no wiki summary.
1
vote
1answer
39 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
40 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
58 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
29 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
75 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
24 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
28 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
0answers
48 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
27 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
0answers
31 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
54 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 ...
3
votes
2answers
86 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?
...
0
votes
1answer
39 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
77 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
75 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
48 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
39 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
91 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
97 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
61 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:
...
1
vote
1answer
76 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 ...
3
votes
0answers
137 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
121 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
55 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
66 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
71 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 ...
10
votes
1answer
468 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
150 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
162 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
361 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
271 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
68 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
134 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
158 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 ...
1
vote
1answer
143 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 ...
2
votes
2answers
440 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 ...
12
votes
2answers
714 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
95 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)))?
...
6
votes
2answers
455 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
294 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 ...
0
votes
2answers
368 views
How can I determine the cardinality of a set of polymorphic functions?
It seems obvious to me that the set of functions with the signature $\forall A. A \rightarrow A$ is "once-inhabited", i.e. there is only one such polymorphic function which "works" for any set $A$, ...
0
votes
1answer
158 views
How are fractional numbers most effectively encoded in lambda calculus?
I haven't been able to find any information on this, but I think that if someone knows it, it's someone here. I need it for some theoretical knowledge about lambda calculus and compiler optimizations.
...
2
votes
1answer
156 views
Styles of logical systems
There are few well-know styles of logical systems (LS): Hilbert-style, Sequent-style, Natural deducton style. And such lesser-know styles as Gottlob-Frege two-demensional notation, systems with ...
1
vote
1answer
189 views
Inductively Defined Family of Sets
Suppose I am given the following inductive definition$^1$: Let $T$ be the smallest family of sets $\{T_1,T_2,T_3,\ldots\}$ such that
$0 \leq k < n \Rightarrow k \in T_n$
$t_1 \in T_n \wedge n ...
0
votes
1answer
343 views
lambda calculus, equalities
Help would be appreciated. The notes are poor on the subject, and im clueless.
Verify the following equalities:
A) SIII=βI, where S is λxyz.(xz)(yz) and I is λx.x
B) twice (twice) f x= β f(f(f(f ...
0
votes
2answers
569 views
Proving a combinator is a fixed point
Show that the term ZZ where Z is λz.λx. x(z z x) satisfies the requirement for fixed point combinators that ZZM =β M(ZZM).
6
votes
1answer
741 views
The Power of Lambda Calculi
A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions.
What are the advantages of typed lambda calculus over untyped lambda calculus in ...
23
votes
6answers
2k views
Learning Lambda Calculus
What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus?
Specifically, I am interested in the following areas:
Untyped lambda calculus
...
