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
40 views

Beta reduction: how to?

I'm trying to beta-reduce the following: $$\lambda xy.y((\lambda xyz.xyz)(\lambda u.u)(\lambda u.uu))$$ Anyway I think that I didn't understand terms' scope. Considering the application in the shape ...
0
votes
1answer
15 views

Why is this lambda calculus expression already in normal form?

I don't quite follow why the following expression is in normal form $$\lambda y.(y (\lambda z.w) (\lambda z.w))$$ I would have thought that reduces to $\lambda y.y w$, but according to ...
3
votes
3answers
114 views

Fixed point combinator and functions with no fixed point

In lambda calculus the fixed point combinator is defined as: It is very easy to see how $Yg =g(Yg)$ for any $g$ by using $\beta$-reduction. At the same time I wonder what is the meaning of ...
1
vote
1answer
28 views

Calculating $(\lambda x.(x+y))1$

$(\lambda x.(x+y))1$ returns(I think): $(1+y)$. Is $(1+y)$ another lambda function so I'd write: $\lambda y.(1+y)$ or is it just $(1+y)$ and if so what does that mean?
1
vote
2answers
65 views

In lambda calculus, why do we define $n=\lambda f.\lambda x.f^n(x)$ instead of $n=\lambda f.f^n$?

I just started learning lambda calculus and I understood most of it but i was thinking that why do we define $n=\lambda f.\lambda x.f^n(x)$ instead of $n=\lambda f.f^n$? I think it would be more ...
1
vote
1answer
48 views

In lambda calculus, can the parameter of abstraction be a non-variable lambda expression?

In short, my main confusion is between the two concept variable and lambda expression: I am reading this reference here: ...
3
votes
0answers
47 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
2
votes
2answers
47 views

In what sense is the S-combinator “substitution”?

According to the Wikipedia page on SKI-combinator calculus, I is the identity function, K is the constant function, and S is "substitution". I understand the first two, but I don't see what S has to ...
3
votes
2answers
100 views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
3
votes
1answer
120 views

What does “calculus” mean?

"calculus" and "formal system" From http://en.wikipedia.org/wiki/Propositional_calculus#Terminology a calculus is a formal system that consists of a set of syntactic expressions ...
1
vote
0answers
51 views

Is this proof for the undecidability of $\beta$-normalisation in $\lambda$-calculus valid?

The proofs I have so far seen for the undecidability of $\beta$-normalisation all make use of Gödel numbering in order to first prove the more general Scott-Curry theorem. As an exercise, I have tried ...
6
votes
1answer
128 views

How to prove that these are the only type inhabitants?

Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ with its two inhabitants \begin{align} \mathrm{tt} &= \lambda x.\ \lambda y.\ x \\ \mathrm{ff} &= \lambda ...
0
votes
1answer
32 views

Lambda calculus reducing expression

I have following expression to reduce: (λmnfx.mf(nfx) λfx.fx λzy.zzy) After some substitutions i get the result: ...
1
vote
1answer
46 views

Lambda calculus expression reduction

I don't know the correct answer how this reduction should've be done. Should I simply put λfx.fx in a place of m and λzy.zzy in a place of n? ...
2
votes
2answers
41 views

Understanding η-conversion (Lambda Calculus)

Let $h \in A\rightarrow (B\rightarrow C)$ I'm trying to understand the following reduction: $$\lambda x\in A. \lambda y \in B.(h(x))(y) \\= \lambda x\in A.h(x) \\= h$$ Apprantly, this is done by ...
0
votes
1answer
70 views

Extensional versus intensional theories in mathematics

Lambda calculus is often cited as an intensional theory whereas set theory is cited as an extensional theory. What are other examples of extensional and intensional theories of mathematical logic?
5
votes
1answer
77 views

Proving that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus

I am trying to prove that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus. Surprisingly, different textbooks and lecture notes do not contain that proof, ...
2
votes
0answers
30 views

Chaitin's constant for lambda calculus and combinatory logic

I have found some approximations of Chaitin's Constant for turing machines but I have not found approximations for others. I'd like to have a rough estimate or upper bound on it for lambda calculus ...
4
votes
1answer
84 views

What's the definition of equational theory? Why is λ logic free?

A book says that "λ is logic free: it is an equational theory." But I don't understand the "logic free" and "equational theory". Can you help me?
1
vote
1answer
38 views

Lambda calculus: encoding lists and projectors

Given a pair $[M_1,M_2]$ there is an easy encoding $\lambda x.x M_1 M_2$. For the n-tuple we have two options. First encoding: $$\lambda x.x M_1, M_2, \ldots , M_n$$ Second encoding: $$[M_0, [M_1 , ...
0
votes
1answer
62 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
128 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
97 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
36 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
51 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
70 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
2answers
115 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 ...
2
votes
1answer
83 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
44 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
33 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
56 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
92 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
46 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
78 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
76 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
33 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
70 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
77 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
55 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 ...
0
votes
0answers
15 views

Extracting values out of functions

Suppose that we add "typed" values into the untyped lambda calculus. Is it always possible to convert a lambda abstraction to it's equivalent typed value (like l y . 2 y becomes 2) without giving ...
4
votes
3answers
111 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
54 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
57 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
43 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
108 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
140 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
33 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 ...
7
votes
4answers
173 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
243 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
80 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?