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

Substitution of variable with term including unbound but used variable - refactor?

λx.y[x:=y] == λx.y since x is bound, no substitution happens. But what about λx.y[y:=x]? ...
2
votes
1answer
102 views

Wikipedia's explanation of the lambda-calclulus form of Curry's paradox makes no sense

Wikipedia gives multiple explanations of Curry's paradox, one of which is expressed via lambda calculus. However, the explanation doesn't look like any lambda calculus I've ever seen, and there's an ...
2
votes
2answers
120 views

How to define $f(x) = 2x$ as a recursive and lamba function?

How can I exhibit a recursive function and a $\lambda$-term simulating the function $f : \mathbb{N} \rightarrow \mathbb{N}$, such that $f(x) = 2x$? For $\lambda$ part, I thought to create a mult ...
0
votes
0answers
21 views

How to prove Y Y = Y (Y(Y))

I found a prove online, but I can not fully understand it. The prove is like this: let Y = lambda y . (lambda x . y (x x)) (lambda x . y (x x)) ...
1
vote
0answers
10 views

Examples of Partial Combinatory Algebras with surjective pairing?

What are some good examples of partial combinatory algebras (a.k.a. Schoenfinkel algebras) with surjective pairing? I mean this in the sense that, if $\mathsf{D}$ is the pairing combinator and ...
1
vote
1answer
23 views

Understand free and bound variable associations in Lambda Calculus

I understand that free variables in Lambda calculus are those that are not bound to a specific metavariable inside of an abstraction, while bound variables are the direct opposite. The idea that ...
0
votes
0answers
14 views

Finding the lambda-closure and transition function?

so lets say that we have a lambda-NFA given by the following transition table: ...
3
votes
0answers
25 views

Extensionality of a hierarchy of functionals over $\mathbb{N}$

Let $H$ be the complete hierarchy of functionals over $\mathbb{N}$. To be precise: let the set $T$ of 'simple types' be the smallest set such that '0' $\in T$ and $(α→β) \in T$ whenever $α, β \in T$. ...
0
votes
0answers
26 views

Is there a connection between the y combinator (fixed point combinator) and eigenvectors/values?

It recently occurred to me that a fixed point in lambda calculus sort of has the same feel as an eigenvector/value in linear algebra. In the case of a fixed point function you have a function and a ...
2
votes
1answer
28 views

notation for substitution in lambda calculus

I think I get the substitution notation in lambda calculus for "simple" applications such as: (λx.x+1)(5)=[5/x](x+1)=5+1=6 What I don't get is how that works ...
2
votes
1answer
55 views

Book on Curry-Howard Isomorphisms

I would like to learn about Curry-Howard Isomorphism because I want to know more about connections between computability and logic. I have already read book on first order logic and I know about ...
0
votes
0answers
28 views

Book/Text recommendation Lambda Calculus and Cartesian Closed Category

Could anyone recommend a good resource (introductory, built from basic) to learn about lambda-Calculus and its relation with Category theory? I don't have any background in Computer Science, but most ...
0
votes
2answers
49 views

lambda calculus, definition of true and false

Are the following lambda-calculus definitions axiomatic? true: $\lambda xy.x$ false: $\lambda xy.y$ Is the definition truly arbitrary? In my impression, it looks like we could just swap the ...
2
votes
1answer
42 views

Hindley's “Introduction to combinatory logic”, exercise 6 chapter 2.

Can somebody help me with the following exercise? Find a combinator X such that X = S(KK)(XS). Reduction rules are usual: IX reduces to X (identity combinator) KXY reduces to X SXYZ reduces to ...
0
votes
0answers
44 views

Are elimination of lambda and closure expressions always possible?

As proofed the lambda calculus, which uses higher-order functions (passing functions as arguments), is turing complete. This makes me wonder if one of the following statements is true: Are ...
0
votes
1answer
25 views

Map a set with it's index

Let's say I have the set: $$ A = \{1,2,3,4\} $$ How would I express something like this: ...
0
votes
1answer
36 views

Do λ-terms form a group with composition?

Consider obviously as composition the well known combinator $\circ := \lambda f g.\lambda x.f(g x)$. It is easy to see that it associates ($\circ(\circ f g)h \equiv \circ f(\circ g h)$), and that it ...
0
votes
0answers
23 views

What is this P4 correspond to in proposition as types?

I was reading "Proofs and Types", so there came across that any proposition can be converted to lambda form. So was trying out with Hilbert system's axioms P1. $A \rightarrow A $ P2. $A \rightarrow ...
0
votes
0answers
11 views

Formulation of arithmetics without an actual implementation of Church numerals

Starting from the definition of Church numerals given on Wikipedia (that is, a succession of $\lambda$-terms $c_n \mid c_n f x \equiv f^{n}x$), I have two questions: Is $c_n := ...
3
votes
1answer
33 views

In lambda calculus what is the correct definition of numbers

As a programmer I have been diving into functional programming and am therefore interested about the math behind all of the languages. I had a small course of lambda calculus at university, but ...
2
votes
1answer
43 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
19 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
28 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
29 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
41 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
73 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
47 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 ...
3
votes
2answers
98 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 ...
1
vote
2answers
65 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
2answers
77 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
96 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
164 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
52 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
1answer
117 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
148 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
98 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
40 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
36 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
48 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
79 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
38 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
54 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
28 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
56 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
80 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
86 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
25 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
133 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
107 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
60 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. ...