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

Find a lambda-expressions F, K such that for all M, FM = F and KM = MK

Find a lambda-expression F such that for all M, FM = F Find a lambda-expression K such that for all M, KM = MK My guess is to somehow use the combinator Y := \f. (\x.f(xx))(\x.f(xx)) so that YF = ...
1
vote
0answers
27 views

Counting Reals with the Lambda Calculus

I have come up with an explanation for the countability of the reals and I am wondering where I went wrong. In the lambda calculus, all integers can be represented by functions fairly simply. ...
2
votes
0answers
23 views

When does renaming bound variables require a fresh variable?

Suppose that $E_1$ and $E_2$ are two $\alpha$-equivalent first-order logic formulas (or $\lambda$-terms), and let $V$ be the set of all variables (free and bound) used in $E_1$ or $E_2$. Is it ...
1
vote
0answers
26 views

Deriving the fixed point for $\omega$ (i.e. $\lambda x.xx$) and proving it to be so

I am studying the simply typed $\lambda$-calculus, and I am struggling a bit with really understanding fixed-points and the $\mathbf Y$ combinator. I have read or skimmed all the questions on here ...
4
votes
0answers
36 views

What is the actual significance of the lambda calculus for the formalization of math?

The Simply Typed Lambda Calculus was proposed initially as a foundational system for the formalization of mathematics. As such, I would expect that soon there would be attempts to implement most of ...
1
vote
0answers
19 views

Solve recursive equation in lambda calculus

I need to find such F, so that for any M $FM = MF$. I can't figure out, how to bring this equation to the form like this: $F = TF$, so that I could just apply Y combinator
3
votes
0answers
38 views

Is there any elegant formalization of fractional numbers?

The question is just what is on the title, but I'll describe the context for completion: Natural numbers can be encoded quite elegantly on the Lambda Calculus as church numbers, that is, a function ...
3
votes
1answer
34 views

How high up do kinds go in type theory?

I understand this is a bit naive, but I just learned how types can have types that we call 'kinds,' in system F$\omega$ as a sort of extended higher order lambda calculus. The wiki article on it ...
1
vote
2answers
46 views

why would you use lambda calculus over other forms of function notation?

What does "$\lambda x.x$" offer that "$f(x)=x$" can't cover? More generally, when would we want to represent a function through lambda calculus over another form of function notation?
1
vote
1answer
18 views

Proof of B, C, K, W system

There is a B,C,K,W system. In particular, there is presented the following identity: $B = S (K S) K$ How to prove this statement?
1
vote
0answers
44 views

Do I really need lambda abstraction for type theory?

So I think I somewhat understand the type theory of the various lambda calculi in the lambda cube, from the simply typed lambda calculus to the calculus of constructions, but looking at it I'm ...
1
vote
1answer
80 views

zero raised to power zero in Church encoding

In Church encoding of the natural numbers in lambda calculus raising zero to the power zero gives the answer zero. Does anybody know of an encoding where the answer is 1?
0
votes
1answer
26 views

Lambda Calculus Reduction (applicative vs normal order)

I am a little confused to reduce these lambda calculus expressions. I am instructed to give applicative and normal order reductions for these expressions. (a) (λx. ((λy.(* 2 y)) (+ x y)))y (b) (λx. ...
2
votes
0answers
44 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
22 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
28 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
40 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
30 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
49 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
52 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
52 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
40 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
35 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
27 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
24 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
45 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
33 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
67 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
166 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
55 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
22 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
166 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
82 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
56 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
64 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
79 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
124 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
163 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
63 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 ...
7
votes
1answer
139 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
37 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
54 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
47 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
81 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
41 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
98 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
44 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 , ...