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
1answer
35 views

Is the combinator $\mathbf{SI}$ typable (à la Curry)?

Consider the combinators $\mathbf{S} \equiv \lambda xyz . xz(yz)$, $\mathbf{I} = \lambda w.w$ and their application $\mathbf{SI}$. Is this term typable à la Curry? From what I did so far, it seems it ...
2
votes
0answers
13 views

Find recursively enumerable theory $\mathcal{T}_3$ such that $\mathcal{T}_1 \subsetneq \mathcal{T}_3\subsetneq \mathcal{T}_2$.

I am trying to solve the following problem: Let $\mathcal{T}_1, \mathcal{T}_2$ be recursively enumerable $\lambda$-theories such that $\mathcal{T}_1 \subsetneq \mathcal{T}_2$. Show that there ...
2
votes
1answer
15 views

Does $\beta \eta$ reduction preserve free variables?

It seems to be a know fact that if $M$, $N$ are $\lambda$-terms, and $M \twoheadrightarrow_{\beta\eta} N$, then $fv(N) \subseteq fv(M)$. My problem is: is it true that if $M ...
1
vote
0answers
25 views

A kind of reverse Church-Rosser

In the $\lambda$-calculus. Proposition: For any terms $M$,$N$ such that $M =_\beta N$, there is a term $L$ such that $L \twoheadrightarrow_\beta M$ and $L \twoheadrightarrow_\beta N$. Is this true ...
0
votes
0answers
26 views

Lambda calculus Beta reduction

When applying Beta reduction does the function also affect on the $\lambda$ term? (If same value) For example $\lambda$ z.$\lambda$ z (z z) t What is the correct reduction? $\lambda$z (t t) ...
4
votes
1answer
52 views

What breaks the Turing Completeness of simply typed lambda calculus?

On the Wikipedia page about Turing Completeness, we can read that: Although (untyped) lambda calculus is Turing-complete, simply typed lambda calculus is not. I am curious as to what exactly ...
2
votes
1answer
35 views

Meta-introduction for implication in Natural Deduction for intuitionistic Propositional Logic

I am going through a paper entitled A Tutorial on the Curry-Howard Correspondence by Darryl McAdams. The author defines a ternary notation as follow to easily manipulate proof trees (page 6 - line ...
2
votes
2answers
75 views

Are untyped and simply typed lambda calculus mutually exclusive?

In "Proposition as Types" by Philip Wadler we can read that: The two applications of lambda calculus, to represent computation and to represent logic, are in a sense mutually exclusive. If ...
0
votes
2answers
31 views

Self-application in Church's untyped lambda calculus

In "Proposition as Types" by Philip Wadler mentions the weaknesses of untyped lambda calculus and "Russell's logic" concerning self-application. Whereas self-application in Russell’s logic leads ...
2
votes
1answer
42 views

Encode lambda calculus in arithmetic?

There is plenty of information about how to encode arithmetic given the lambda calculus. The wikipedia article on Church Encoding seems complete to my inexpert eye. My question is "how about the ...
0
votes
1answer
78 views

Define inl : $σ → σ ∨ τ$

I'm a bit stuck in Geuvers' "Introduction to Type Theory" (http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf), p. 39: Exercise 13. Prove the derivability of some of the other logical ...
0
votes
1answer
141 views

Lambda calculus typing

I'm trying to find a type T such that I can create a derivation tree for the following expression: λx.λy.((xy)y) : T Am I right in thinking that there is no such T for this to be possible? If I'm ...
0
votes
1answer
28 views

Simple Problem with Lambda Calculus and Y Combinator

I am currently reading about the lambda calculus as well as the Y combinator. I know that for any function $f$, $Yf$ is a fixed-point of $f$, that is $f(Yf) = Yf$. In order to wrap my head around ...
0
votes
0answers
28 views

Showing equality of two lambda calculus expressions

I need to show the beta-equality of three lambda terms, but I'm not able to: $(λx y z:(xz)(yz)) λu:u \stackrelβ= (λv:v λy z u:u) λx:x$ $(λx y:x λz:z) λa:a \stackrelβ= (λy:y)λb z:z$ $λx.Ω \stackrelβ= ...
0
votes
1answer
54 views

Barendregt's Substitution Lemma (lambda calculus)

I am struggling to put words on an idea used in Barendregt's Substitution Lemma's proof. (available here) The lemma states that: If x≠y and x not free in L and M, L are $\lambda$-terms: then ...
2
votes
1answer
38 views

Doing alpha conversions and beta reductions, Lambda Calculus

I am attempting to perform Lambda calculations. I have the following information. T = $\lambda xy.x$ F = $\lambda xy.y$ A = $\lambda xy.xyF$ I attempted to perform Beta reduction and alpha ...
0
votes
1answer
90 views

question about lambda calculus

I'm triyng to understanding lambda calculus but I have some difficulty espacially when websites or books I search starts to make things a bit more complicated. what I've understood by now is: given ...
0
votes
1answer
38 views

Lambda Calculus: Prove $m \ Succ\ n = m+n$

Given $Succ = \lambda n. \lambda fx. f(n f(x))$ and church's numeral: $n = \lambda fx.f^n(x)$ Show that $ m\ Succ\ n = m + n$ I don't get how it can be shown. I get stuck on this step: $\lambda ...
0
votes
1answer
27 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
32 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
43 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
32 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 ...
6
votes
0answers
49 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
23 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
5
votes
0answers
49 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 ...
4
votes
1answer
51 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
57 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
20 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?
2
votes
1answer
94 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
93 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
44 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
51 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
26 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
30 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
55 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
31 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
55 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
64 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
77 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
44 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
47 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
31 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
49 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
36 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
78 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
190 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
57 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 ...