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

Problem understandig lambda-calculus incompatible problem.

Let $K \equiv \lambda xy.x$ and $S \equiv \lambda xyz.xz(yz)$. Show that S and K are incompatible. The solution goes like: Let $S=K$ and $I \equiv \lambda x.x$, we have to show that all terms are ...
3
votes
0answers
24 views

Can all computable numeric functions on church numerals in ski-combinator calculus be expressed using only completely evaluated terms?

Let a term in ski-combinator calculus be called "complete" if every primitive is partially applied (so all S's are applied to at most two arguments, all K's to at most 1, and all I's are not applied). ...
1
vote
0answers
17 views

Equivalence of Turing Machines and Lambda Calculus

Based on the Church Turing Thesis, we conjecture that Turing Machines are the "correct," model of computation. It is well known that they are equivalent to the Lambda Calculus, another model of ...
1
vote
1answer
22 views

On the Y-Combinator in Lambda Calculus

I am trying to follow this explanation on the Y-combinator Fairly at the beginning the author shows this function definition and claims that ...
1
vote
1answer
24 views

lambda calculus: predecessor function

Apparently this expression can be used to calculate the predecessor of a given church numeral: $\renewcommand{\l}{\lambda}$ $\l n.(n\ \l p . (p.2,\ s p.2)\ (\overline{0},\ \overline{0})).1$ ...
1
vote
0answers
32 views

Graph of a higher-order function

When we deal with functions which work on numbers, we can graph them easily: Just take each of its possible input values and find its corresponding point on one axis, then go straight up in its ...
1
vote
0answers
32 views

What is the root of first class object in programming languages?

What is the root of "first class object" of programming languages? (Also see https://en.wikipedia.org/wiki/First-class_function, and ...
0
votes
0answers
17 views

Substituition Lemma proof's in lambda Calculus

I am trying to proof of Substituition Lemma in , but I have some doubts: The Lemma states thats: If $x \not\equiv y, x \notin FV(t_2) $, then $t[x /t_1][y/t_2] \equiv t[y/t_2][x/t_1[y/t_2]]$. The ...
1
vote
0answers
57 views

I did not understand one thing in the proof of substitution lemma?

The substitution lemma in lambda-calculus is proved by the following way, but I just did not understand the application of induction hypothesis in it. The lemma as shown below, where x and y are ...
5
votes
0answers
123 views

Injections between distinct models of the simply typed lambda calculus

Let a model of the simply typed lambda calculus be a Cartesian-closed functor from $C_T$ to Set, where $C_T$ is a free CCC (as in e.g. this reference, p. 83.) The simple case of one or two primitive ...
0
votes
1answer
34 views

Trouble solving lambda calculus example

Let $M \equiv \lambda xy.y(xx)$, then what is $MM(\lambda z.M)$. I tried and i got a recursion, but I know the answer should be M. Thanks in advance.
2
votes
2answers
68 views

Relation between Cartesian closed category and Lambda Calculus

I am programmer (from the object oriented world) and currently getting my head around functional programming. I was looking to get some basics right. I understand what category theory and lambda ...
0
votes
2answers
43 views

How to define numbers in a way that a number 'n' is equivalent to the function plus 'n'?

In lambda calculus, is it possible to define (or disprove the existence of) a number system alternative to church numerals such that each number is a function which on application, adds itself to it's ...
1
vote
2answers
72 views

Distinguishing pure, closed lambda terms

Let $M$ be a full model of the simply typed lambda calculus, over some collection of base types, with the constraint that $|D_\sigma|\geq 2$ for each base type $\sigma$. Let $a$ and $b$ be two closed ...
1
vote
1answer
41 views

Lambda Calculus Proof: or false (not true) Evaluates to False, using lazy evaluation, Help!

I am trying to learn lambda calculus, and I am currently tackling a few boolean logic questions. I have gotten to one that I am stuck on, and I am looking for a little help proceding. I need to ...
0
votes
1answer
25 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]? ...
4
votes
1answer
121 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
136 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
1answer
39 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
31 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
22 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
31 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
30 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
63 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
34 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
55 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
47 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
54 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 ...
-1
votes
1answer
31 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
38 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
29 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
12 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
34 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
48 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
23 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
32 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
33 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
1answer
46 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
91 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
50 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
111 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
89 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
97 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
98 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 ...
1
vote
1answer
171 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
63 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
178 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
202 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 ...