The tag has no wiki summary.

learn more… | top users | synonyms

2
votes
2answers
33 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
87 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
105 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
48 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
125 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
30 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
43 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
40 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
67 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
61 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
28 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
78 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
37 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
60 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
105 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
87 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
35 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
50 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
67 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
2answers
112 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
0answers
69 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
41 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
27 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
50 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
91 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
42 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 ...
2
votes
1answer
71 views

Simple type theory: Proof inexistance of closed term

In simple type theory, how can I prove that there is no closed term of type? $$((P \Rightarrow Q) \Rightarrow Q) \Rightarrow P$$
2
votes
1answer
73 views

Consequences of difference between “strong” and weak Church-Rosser property

An Abstract rewriting system is a set A, whose elements are usually called objects, together with a binary relation on A, traditionally denoted by $\rightarrow$. An object $x \in A$ is ...
1
vote
0answers
30 views

Reductions under lambda in dependently typed lambda calculus

I am currently reading a Simon Thompson's Type Theory book. In chapter 5 he introduces a system TT(0,C), which limits a notion of reduction . In this notion of reduction, reductions under lambda are ...
2
votes
1answer
66 views

Is Lambda calculus a purely equational theory?

In a previous question I have been told that lambda calculs is pure syntax. I see that Lambda calculus is introduced inductively, but I don't see from what axioms it follows that: $$(\lambda x.x) M ...
1
vote
2answers
69 views

Meaning of variables and applications in lambda calculus

The wikipedia definition of lambda terms is: The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms: a variable, $x$, is ...
0
votes
2answers
55 views

Understanding second axiom of Primitive recursion

I read about Primitive recursion and was able to understand most of it. However I am finding it very difficult to understand the second axiom of primitive recursion. I can make out that it helps in ...
0
votes
0answers
15 views

Extracting values out of functions

Suppose that we add "typed" values into the untyped lambda calculus. Is it always possible to convert a lambda abstraction to it's equivalent typed value (like l y . 2 y becomes 2) without giving ...
4
votes
3answers
100 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
1
vote
1answer
52 views

Is it possible to reduce a lambda expression to it's smallest equivalent form?

In the Untyped Lambda Calculus, is it possible to reduce any arbitrary expression to it's smallest equivalent form? (defined as an expression with the smallest number of lambda terms) If so, is there ...
2
votes
1answer
53 views

Lambda calculus - function reduction

I am trying to learn how to reduce functions in $\lambda$ calculus and I came across this task: Reduce this expression using normal strategy and applicative strategy. $(\lambda x.\lambda ...
2
votes
1answer
43 views

Formulate boolean logic in lambda calculus

I want to formulate the boolean operator $\Leftrightarrow$ in lambda calculus. I know that the negation is formulated as $\lambda x.x F T$ and the conjugation is formulated as $\lambda x y.x y F$ as ...
1
vote
0answers
92 views

Associative, commutative properties and identity elements of non-binary functions

I'm making a compiler (for a new language) wich supports AC unification via pattern matching. The matching algorithms already works but i'm having trouble with the logical and mathematical aspects of ...
1
vote
1answer
110 views

Addition within lambda calculus

I've been reading "The Emperor's New Mind" by Roger Penrose. He briefly introduces lambda calculus (pp. 86-92) and gives this formula for addition: $A = \lambda fgxy.[((fx)(gx))y]$ This was my ...
0
votes
1answer
33 views

Prove that $[x/x] M \equiv M$

I just started reading the book Lambda-Calculus and Combinators An Introduction. Using this definition of Substitution in Page 7. I want to prove that if $M$ is any term $[x/x] M \equiv M$. In the ...
7
votes
4answers
163 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
2
votes
1answer
173 views

How to multiply in Lambda Calculus?

I have trouble, when attempting to multiply Church numerals with lambda. First, does this work? MULT := $\lambda$mnfx.m ( PLUS n ) MULT := $\lambda$mnfx.m ( m SUCC n ) MULT := $\lambda$mnfx.m(m ...
0
votes
2answers
61 views

Lambda expression Evaluation

( (λf.λx.f(f(x)))(λy.y ^2 ) ) (5) I tried finding out the order of evaluation for this lambda expression. How is this lambda expression evaluated?
2
votes
1answer
150 views

lambda calculus and category theory

I am not particularly knowledgeable in either lambda calculus or category theory, but I am starting to learn Haskell so I would like to ask: are there connections between category theory and lambda ...
0
votes
1answer
59 views

beta reduction bascis

Hi I get the basics of beta reduction e.g. $$(\lambda var.body)arg $$ you just replace the occurrences of var with arg in body. However what happens here? $$(\lambda x.xx)(\lambda x.xx) ...
1
vote
1answer
54 views

Lambda Calculus: Reduction to Normal Form

I'm working on some problems where I'm supposed to reduce lamda terms to normal form. I'm not sure if I'm doing it right so if someone could let me know, that would be awesome. $$(\lambda x.\lambda ...
0
votes
1answer
50 views

Lambda Calculus: Reducing to Normal Form

I'm having trouble understanding how to reduce lambda terms to normal form. We just got assigned a sheet with a few problems to reduce, and the only helpful thing I've found is the following example ...
4
votes
1answer
74 views

$Mx =_{\beta\eta} Nx$ implies $M =_{\beta\eta} N$

In the context of $\lambda$-calculus, I was thinking about whether or not $$Mx =_{\beta\eta} Nx \implies M =_{\beta\eta} N$$ if $x\notin FV(M)\cup FV(N)$. I have been around this issue for quite some ...
1
vote
2answers
144 views

$\beta$ - conversion and $\alpha$-reduction problem in $\lambda$-calculus

Here is an expression that I am trying to reduce and my operations so far: $$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ...
0
votes
1answer
56 views

Is this $\beta$-reduction well defined?

Would it be possible to apply $(\lambda x.\lambda y. x)$ to the argument $y$? It seems to me that this must not be possible as it would give a different answer if applied to a constant, call it ...