For questions on the formal system in mathematical logic for expressing computation using abstract notions of functions and combining them through binding and substitution.

learn more… | top users | synonyms

0
votes
1answer
87 views

Lambda Calculus using $\beta$-reductions

Use $\beta$ reductions to compute the final answer for the following $\lambda$ terms. Use a "fake" reduction step for "+" operator. Identify each redex for $\beta$-reduction steps. Does the order in ...
1
vote
1answer
237 views

Lambda calculus logical operators

Define the and operator in lambda calculus and prove your definition Define the exclusive or operator in lambda calculus, and prove your definition My answer for #1 is: AND $\equiv$ ...
1
vote
2answers
111 views

Using Combinators in Lambda Calculus

K $\equiv$ $\lambda$xy.x S $\equiv$ $\lambda$xyz.((xz)(yz)) Prove that the identify function I $\equiv$ $\lambda$x.x is equivalent to ((S K) K) I have no clue where to even start for ...
1
vote
1answer
44 views

The approximation rule implies the equality rule in systems of type assignments

I'm reading Barendregt's Lambda calculi with types (1992). In Proposition 4.1.4.1., he "proves" a lemma which shows the approximation rule implies the equality rule in typed lambda-calculi à la ...
0
votes
1answer
57 views

Clarification about the definition of term algebras

The following definition has been given in this article. A term algebra is an algebra $ \langle \mathcal{S}, \mathcal{G} \rangle $ where every time that $g_\alpha, g_\beta \in \mathcal{G}$ and $$ ...
3
votes
1answer
78 views

Why use *λx.x* instead of *f(x)*?

In my semantics class, we're learning about using (abusing?) lambda calculus. So far the professor hasn't imparted any reason for using λx.x instead of using f(x). Why use lambdas instead of basic ...
3
votes
3answers
137 views

How can I prove a simple eta-conversion?

I would like to prove the following: $$\lambda x.\ \lambda y.\ f\ z\ x\ y \overset{\eta}{=} \lambda x.\ f\ z\ x$$ Definitions Free variables $x \in FV(f) :\Leftrightarrow$ $x$ is a variable used ...
3
votes
2answers
139 views

Representing lists and trees in System F

System F (also known as second-order lambda calculus or polymorphic lambda calculus) is defined as follows. Types are defined starting from type variables $X, Y, Z, \ldots$ by means of two ...
0
votes
2answers
46 views

About the definition of fixed-point combinators

I am reading this wikipedia page to understand Fixed-point combinators: In computer science, a fixed-point combinator (or fixpoint combinator[1]) is a higher-order function y that satisfies the ...
0
votes
1answer
57 views

Beta reduction exercise question

I am trying to reduce the following $\lambda$-expression: $$(\lambda x.x x) (\lambda y.y x) z$$ So I am reducing to $$(\lambda y.y x) (\lambda y.y x) z$$ That reduces to $$(\lambda y.y x)xz$$ Now ...
0
votes
1answer
67 views

Pure Lambda Calculus: Call-by-value Free Variable Argument Application Reduction

In pure lambda calculus, under the call-by-value reduction strategy, a term of the form $(\lambda x. x)y \rightarrow y$ implies that the free variable $y$ is a value. However, only abstractions are ...
6
votes
0answers
101 views

Equivalence of categories of directed complete posets

In the book ``Domains and Lambda-Calculi'' by Amadio and Curien, there is the following exercise: Define an equivalence between the category of partial morphisms generated by $(\mathcal{M}_S, ...
0
votes
0answers
51 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in $\lambda\pi $ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$? Note on notation: The epsilon ...
2
votes
1answer
90 views

Simple type theory: Proof inexistance of closed term

In simple type theory, how can I prove that there is no closed term of type? $$((P \Rightarrow Q) \Rightarrow Q) \Rightarrow P$$
2
votes
1answer
95 views

Consequences of difference between “strong” and weak Church-Rosser property

An Abstract rewriting system is a set A, whose elements are usually called objects, together with a binary relation on A, traditionally denoted by $\rightarrow$. An object $x \in A$ is ...
1
vote
0answers
39 views

Reductions under lambda in dependently typed lambda calculus

I am currently reading a Simon Thompson's Type Theory book. In chapter 5 he introduces a system TT(0,C), which limits a notion of reduction . In this notion of reduction, reductions under lambda are ...
2
votes
1answer
76 views

Is Lambda calculus a purely equational theory?

In a previous question I have been told that lambda calculs is pure syntax. I see that Lambda calculus is introduced inductively, but I don't see from what axioms it follows that: $$(\lambda x.x) M ...
1
vote
2answers
88 views

Meaning of variables and applications in lambda calculus

The wikipedia definition of lambda terms is: The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms: a variable, $x$, is ...
0
votes
2answers
61 views

Understanding second axiom of Primitive recursion

I read about Primitive recursion and was able to understand most of it. However I am finding it very difficult to understand the second axiom of primitive recursion. I can make out that it helps in ...
4
votes
3answers
127 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
1
vote
1answer
55 views

Is it possible to reduce a lambda expression to it's smallest equivalent form?

In the Untyped Lambda Calculus, is it possible to reduce any arbitrary expression to it's smallest equivalent form? (defined as an expression with the smallest number of lambda terms) If so, is there ...
2
votes
1answer
66 views

Lambda calculus - function reduction

I am trying to learn how to reduce functions in $\lambda$ calculus and I came across this task: Reduce this expression using normal strategy and applicative strategy. $(\lambda x.\lambda ...
2
votes
1answer
50 views

Formulate boolean logic in lambda calculus

I want to formulate the boolean operator $\Leftrightarrow$ in lambda calculus. I know that the negation is formulated as $\lambda x.x F T$ and the conjugation is formulated as $\lambda x y.x y F$ as ...
1
vote
0answers
153 views

Associative, commutative properties and identity elements of non-binary functions

I'm making a compiler (for a new language) wich supports AC unification via pattern matching. The matching algorithms already works but i'm having trouble with the logical and mathematical aspects of ...
1
vote
1answer
189 views

Addition within lambda calculus

I've been reading "The Emperor's New Mind" by Roger Penrose. He briefly introduces lambda calculus (pp. 86-92) and gives this formula for addition: $A = \lambda fgxy.[((fx)(gx))y]$ This was my ...
0
votes
1answer
37 views

Prove that $[x/x] M \equiv M$

I just started reading the book Lambda-Calculus and Combinators An Introduction. Using this definition of Substitution in Page 7. I want to prove that if $M$ is any term $[x/x] M \equiv M$. In the ...
8
votes
4answers
292 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
3
votes
1answer
504 views

How to multiply in Lambda Calculus?

I have trouble, when attempting to multiply Church numerals with lambda. First, does this work? MULT := $\lambda$mnfx.m ( PLUS n ) MULT := $\lambda$mnfx.m ( m SUCC n ) MULT := $\lambda$mnfx.m(m ...
0
votes
2answers
134 views

Lambda expression Evaluation

( (λf.λx.f(f(x)))(λy.y ^2 ) ) (5) I tried finding out the order of evaluation for this lambda expression. How is this lambda expression evaluated?
3
votes
1answer
323 views

lambda calculus and category theory

I am not particularly knowledgeable in either lambda calculus or category theory, but I am starting to learn Haskell so I would like to ask: are there connections between category theory and lambda ...
0
votes
1answer
62 views

beta reduction bascis

Hi I get the basics of beta reduction e.g. $$(\lambda var.body)arg $$ you just replace the occurrences of var with arg in body. However what happens here? $$(\lambda x.xx)(\lambda x.xx) ...
1
vote
1answer
65 views

Lambda Calculus: Reduction to Normal Form

I'm working on some problems where I'm supposed to reduce lamda terms to normal form. I'm not sure if I'm doing it right so if someone could let me know, that would be awesome. $$(\lambda x.\lambda ...
0
votes
1answer
59 views

Lambda Calculus: Reducing to Normal Form

I'm having trouble understanding how to reduce lambda terms to normal form. We just got assigned a sheet with a few problems to reduce, and the only helpful thing I've found is the following example ...
4
votes
1answer
89 views

$Mx =_{\beta\eta} Nx$ implies $M =_{\beta\eta} N$

In the context of $\lambda$-calculus, I was thinking about whether or not $$Mx =_{\beta\eta} Nx \implies M =_{\beta\eta} N$$ if $x\notin FV(M)\cup FV(N)$. I have been around this issue for quite some ...
2
votes
2answers
202 views

$\beta$ - conversion and $\alpha$-reduction problem in $\lambda$-calculus

Here is an expression that I am trying to reduce and my operations so far: $$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ...
0
votes
1answer
58 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 ...
0
votes
1answer
361 views

Lambda Calculus: beta-reduction and predecessor function

I'm taking one of my last graduate classes but have been struggling with some reductions in lambda calculus. On our last assignment one of the problems was the following: This question is on defining ...
3
votes
1answer
145 views

Give an example of a program in Simply Typed Lambda that produces Bottom.

I'm not sure how bottom applies to simply typed lambda calculus. not A is a common abbreviation for A -> ⊥ But I see no way to construct a function of that signature within the theory. Edit: A more ...
1
vote
1answer
105 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
63 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
111 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
89 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
68 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
495 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
107 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
149 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
80 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
281 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
67 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
92 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 ...