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

2
votes
0answers
13 views

Fixed point combinator (Y) and fixed point equation

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 on fixed point combinator. In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can be ...
2
votes
1answer
14 views

On a corollary of the Church-Rosser Theorem

In the proof of Corollary 1.41.5 from Hindley-Seldin, $\lambda$-Calculus and Combinators - An Introduction, If $a$ and $b$ are atoms and $aM_1...M_m =_\beta bN_1...N_n$ then $a = b$ and $m = n$ ...
2
votes
0answers
25 views

What strongly normalizing lambda calculi exist that can be integrated with/as logic?

If I'm trying to implement a logical system for deduction based on propositional reasoning, I can start with predicates and quantifiers and functions to obtain first order logic. I can further extend ...
1
vote
1answer
36 views

How do scoping rules work in the Lambda Calculus with nested functions

Let's say I have a lambda expression like this: $$(\lambda a . (ab))(c)$$ It reduces to $$cb$$ But let's say I have a nested function $$(\lambda a . (\lambda x.(ax)))(b)$$ Does this reduce to ...
0
votes
0answers
29 views

Representing “not” in lambda calculus

Is there any lambda function which takes as input a lambda term $\lambda x_1x_2...x_n.f$ which is a function of $n$ variables and produces, $\lambda x_1x_2...x_n.\sim f$ . $\sim$ denotes "not". If we ...
3
votes
1answer
45 views

Why does the fixed point theorem hold for every lambda term?

Can someone give a clear and simple answer for why the fixed point theorem holds for every $\lambda$-term, in contrast with the fact that not all numerical function have a fixed point?
1
vote
1answer
42 views

Can differential calculus (limits, integrals, derivatives) be encoded in lambda calculus?

I am wondering, if the Church-Turing thesis holds (all effectively calculable functions are computable by Turing machines/lambda calculus) and I can compute the limit of a function by hand, what is ...
0
votes
1answer
50 views

Church's first postulate for the foundation of logic

In his paper, A Set of Postulates for the Foundations of logic, Church enumerates a set of postulates that he calls formal postulates. They are all said to be true and free from intuitive logic. ...
2
votes
1answer
36 views

Church's definition of “or” in Lambda Calculus

I have been working through Church's Postulates for the foundation of logic. In the paper he has some four definitions that he will then use in order to formulate the later postulates. If someone ...
1
vote
1answer
21 views

Defining equality function between booleans in lambda calculus

I'm trying to define a function that simulates equality between booleans. To achieve equality operator, I can use the negation operator together with the xor operator, since for two boolean variables ...
0
votes
1answer
23 views

Lambda calculus: How to define a function that simulates $\neg p\vee q$?

I am making my first steps in lambda calculus, so please bear with me. I want to create a lambda function, that given two boolean expressions (either $F$ or $T$ - defined below), simulates the formula ...
0
votes
1answer
20 views

Lambda calculus: Simplifying booleans with beta reductions

I have been doing a homework assignment wherein I have been trying to determine the result of ((or true) false) using beta reduction. I began by writing the entire expression using lambda notation and ...
2
votes
0answers
33 views

How far can-I rewrite in lambda functions?

I am quite new with the lambda calculus. I am experimenting lambda-calculus proofs through the coq proof assistant, but the question I have is not related to coq (I guess). However, I'm going to use ...
0
votes
1answer
32 views

Map a set in mathematical notation

How would express the following JavaScript which takes a set and applies a lambda to each member of the set (resulting in a new set) in mathematical notation? ...
1
vote
2answers
53 views

Lambda calculus: composition of SKI

I am doing some exercises on writing a lambda term as a composition of the terms: S=$\lambda$xyz.xz(yz), K=$\lambda$xy.y, I=$\lambda$x.x. I know that all lambda terms can be written using S K and I ...
7
votes
0answers
133 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
14 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
52 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
21 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
144 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
76 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
52 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
57 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
69 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
117 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
135 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
59 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
131 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
35 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
52 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
46 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
79 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
86 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
35 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
89 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
41 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
75 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
193 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
104 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
42 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
56 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
75 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
132 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
2answers
113 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
49 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
62 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
95 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
50 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 ...