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

7
votes
0answers
198 views

Fixed points in computability and logic

I asked this question on CS.SE, too: http://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic I would like to understand better the relation between fixed point ...
1
vote
0answers
19 views

Union and intersection of Bohm trees

When I study the Bohm tree defined in The Lambda Calculus: Its Syntax and Semantics, H.P. Barendregt, Elseviser,$\cap\Phi$ or $\cup_i(M_i)$ always occurs. But I'm confused about the union and the ...
0
votes
1answer
58 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
24 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
185 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
31 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
86 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
61 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
71 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 ...
3
votes
2answers
102 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
132 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 ...
4
votes
1answer
179 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
66 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 ...
8
votes
1answer
143 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
40 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
55 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
64 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
84 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?
6
votes
1answer
147 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
42 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
111 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
45 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
102 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
319 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
120 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
46 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
60 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
79 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
139 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
170 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
54 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
81 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
82 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 ...
7
votes
0answers
112 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, ...
1
vote
0answers
55 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
100 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
109 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
42 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
81 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
103 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
68 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
141 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
61 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
73 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
55 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
272 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
230 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
310 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
687 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 ...