Questions tagged [lambda-calculus]
λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.
549
questions
0
votes
0
answers
33
views
What are some visual representations of the lambda calculus?
I'm building some teaching tools for teaching the lambda calculus and would like some kind of visual representation of it. I've looked at Alligator Eggs and while it is something very similar to what ...
1
vote
2
answers
57
views
(how) is assignment or binding possible in purely functional languages?
i can't seem to find much info on the following question:
how (if at all) is the fixing of names to values (by binding or assignment) possible in a purely functional system like the lambda calculus?
i'...
- 11
0
votes
0
answers
57
views
Representation of pairs in System F
System F defines the data type pair as:
$$X\times Y := \Pi Z. (X\to Y \to Z)\to Z$$
with:
$$\langle x,y \rangle := \Lambda Z. \lambda p^{X\to Y\to Z}.p \text{ }x\text{ } y$$
Projections are defined:
$$...
3
votes
1
answer
95
views
Expression with fastest growth in lambda-calculus
Well-known example of divergent expression in lambda calculus is big-Omega combinator, defined as (λf. f f)(λf. f f). Although big-Omega is divergent expression, it'...
- 145
0
votes
1
answer
81
views
Valid Lambda Expressions
I have two questions about the validity of lambda expressions.
First, is a variable on it's own a valid lambda expression (ex: λx)
Second, take for example these two lambda expressions (λx.fxya and ...
2
votes
1
answer
37
views
Is it actually the case that $Yg \to_\beta g(Yg)$?
For reference, the $Y$-combinator is the expression
$$ Y = \lambda f . (\lambda x . f (xx)) (\lambda x . f (xx)) $$
in the untyped lambda calculus. If $g$ is any lambda expression, then
\begin{align}
...
- 121
0
votes
0
answers
22
views
Does lambda calculus become covariant if you fix the base type instead of the lambda calculus term?
In category theory, we are taught that polymorphic functions correspond to dinatural transformations, a k a multivariant natural transformations between functors of mixed variance
$\operatorname{G} \...
3
votes
1
answer
137
views
What exactly is delta reduction?
I have found two definitions of delta reduction:
Barry Watson defines it as the result of applying a primitive computation to terms in normal forms
But in Coq they define it as the substitution of a ...
- 165
2
votes
0
answers
40
views
lambda-calculus Church Rosser Theorem and Application Order Reduction
I have a question about an "apparent" contradiction I found in my lesson notes on Application Order Reduction (AOR) and the Church-Rosser Theorem (CRT). I'd like to emphasize that I'm not ...
- 21
3
votes
1
answer
134
views
The Kleene–Rosser paradox and the inconsistency of lambda calculus
In many references I find that the simply typed lambda calculus was introduced because the Kleene–Rosser paradox showed that pure/untyped lambda calculus was inconsistent. However, since it is untyped,...
- 133
0
votes
1
answer
61
views
What is lambda caculus's "fix point combinators" corresponding to Turing Machine?
The lambda caculus equals to Turing Machine,so What is lambda caculus's "fix point combinators" corresponding to Turing Machine?
according to the paper <Primitive Rec, Ackerman's Function,...
- 121
1
vote
0
answers
43
views
Seeking Intuitions about Recursion, Y Combinator and System F
So, as I understand things, System F (polymorphic lambda calculus) doesn't have the Y Combinator and isn't Turing Complete, but it is very expressive. This answer (https://cstheory.stackexchange.com/...
- 11
3
votes
1
answer
74
views
Is shadowing of the type variable allowed in System F second order abstraction?
I'm reading Type Theory and Formal Proof by Nederpelt and Geuvers. Chapter 3 is about $\lambda 2$ and $\Pi$-Types (aka System F, I think?) and the derivation rule for 2nd order abstraction seems to ...
- 165
0
votes
0
answers
52
views
Why, in principle, can a Turing machine describe any computation or procedure?
Why is it that a Turing machine can perform all kinds of calculations and procedures?
As a test, I tried to perform a four-quadratic calculation using a Turing machine myself.
However, although I ...
- 1
7
votes
1
answer
685
views
Strictness in both arguments but not in each individually
I'm learning about strict functions in Haskell.
A function f is strict if f ⊥ = ⊥
Some functions are strict only in the first argument (for e.g. const), others are strict in the second (for e.g. map)....
- 73
1
vote
1
answer
34
views
Are lambda calculus forms with different variable names the same?
Someone suggested to me that the halting problem could be solved by a lambda calculus "program", which reduces to $\lambda y.y$ if an input program halts and $\lambda n.n$ if it does not. ...
- 1,720
-3
votes
1
answer
73
views
Can we solve a decision problem with two identical answers like $false\equiv(\lambda f.\lambda y.y)$ or $0\equiv(\lambda f.\lambda n.n)$?
as the title says
Can we solve a decision problem with two identical answers like $false\equiv(\lambda f.\lambda y.y)$ or $0\equiv(\lambda f.\lambda n.n)$?
if no why? and if yes then why can't we ...
- 73
-1
votes
1
answer
111
views
Why use the term "beta equality"?
In lambda calculus (I will use untyped) if a term containing a redex is beta-reduced to another term, then for some reason they are considered "beta-equal". But the lambda calculus only ...
2
votes
0
answers
50
views
Lambda calculus with unordered application
In lambda calculus, $\lambda xy.\phi$ isn't in general equivalent to $\lambda yx.\phi$. However, it seems possible to imagine a calculus which replaces application with something like specification, ...
- 231
0
votes
1
answer
57
views
How a simple algorithm of adding two numbers can be written in lambda calculus?
It is claimed that "lambda calculus is a universal model of computation that can be used to simulate any Turing machine". How can I, using this universal model, simulate an algorithm of ...
- 113
0
votes
1
answer
59
views
Confusion when composing functions in Lambda expression
$$(\lambda x. x \text{ } x ) ( \lambda x . x \text{ } x )= (\lambda x. x \text{ } x) ( \lambda x . x \text{ } x)$$
Source
I am a bit confused on how this composition was done. When I do it, I get:
$$...
0
votes
0
answers
52
views
If type theory is one of the foundation of Haskell, why can't you call a function in itself?
Consider this following Lambda expression:
$$\lambda s. (s \text{ } s )$$
This function applies it's arguement to it's arguement. If this is a valid lambda expression, wouldn't it also be allowed in ...
0
votes
1
answer
52
views
How to find a term that proves a given proposition?
I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
user157472
1
vote
1
answer
44
views
Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$
Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ...
user157472
0
votes
0
answers
30
views
Where can I find a list of logics with their corresponding calculus and computation phenomena?
I was watching some lectures by Prof. Pfenning on Proof Theory. Between 5:30 and 15:00, he gave a list for some different kinds of judgments along with their calculus and computation phenomena that ...
- 109
0
votes
0
answers
72
views
Goedel's theorem, halting problem and irreducible complexity
I have a vague idea on the tip of my mind that I can only convey through examples.
Gödel's theorem states that some systems (ZFC, for example) are always incomplete in the sense that new axioms (which ...
1
vote
1
answer
57
views
How does "+" operator fit into the formal grammar of $\lambda$-calculus?
In Wikipedia I found out that the formal grammar of $\lambda$-calculus is the following:
...
- 113
1
vote
1
answer
52
views
How is the direct product of the functions (A -> B) * (C -> D) equivalent to the function (A * C) -> (B * D)? Is there an error here?
In the simply typed lambda calculus we have type algebra - types can be added, multiplied and exponentiated, where addition corresponds to the sum type, multiplication to the product type, and ...
1
vote
1
answer
52
views
On the logical and categorical interpretation of lambda calculi and type systems
There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories.
Some variants of Barendregt's pure type systems have the property of strong ...
0
votes
0
answers
24
views
Finding a closed term $t_2$ such that $t_2(λx.x)ss$ = $t_2s$
I'm trying to construct a closed term $t_2$ such that for each closed term $s$, $t_2(λx.x)ss$ = $t_2s$
I know that to solve equations of the shape $. . . u . . .$ = $. . . u . . .$, I'm meant to to ...
- 423
1
vote
1
answer
36
views
Example of preservation failing in Java - follow up question
This is a follow-up question to my previous question
I have been reading this post and it comes up with the following example showing how Java type system is unsound:
...
- 101
1
vote
2
answers
131
views
Example of progress and preservation failing in a commonly used programming language like Java
I am wondering if my solution is correct or I am on the right track. I have searched online and found a paper about Java type system being unsound but that doesn't really answer the progress and ...
- 101
1
vote
0
answers
37
views
Simple Lambda Calculus Question [closed]
For any 2 strongly normalizing terms in the Simply Typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong ...
1
vote
0
answers
23
views
Is it possible to state strong normalization through set inclusion?
In an abstract rewriting system $\langle A, \rightarrow\rangle$, confluence may be stated by using set inclusion. Namely, a rewriting system is confluent iff ${\leftarrow^*\rightarrow^*}\ {\subseteq}\ ...
- 711
1
vote
0
answers
93
views
Can the Calculus of Constructions (without inductives) be used to axiomatize mathematics?
I'm aware that proof assistants like Coq and Agda are based on CIC rather than CoC because there is e.g. no inductive natural number type in CoC. Therefore, for example the proof that addition is ...
- 329
0
votes
0
answers
81
views
Examples of Church Encoding
I am a bit confused by Church Encoding and can't find any practical examples on the internet. I get the formulas for representing numbers and applications but don't understand how applications on ...
- 1
1
vote
1
answer
54
views
Instances of simulating lambda calculus?
There are a ton of resources on the web devoted to proving some esoteric language is Turing complete by simulating arbitrary turing machines. I have an esoteric language I want to prove is complete, ...
- 225
1
vote
0
answers
39
views
Lambda beta-reductions
I am trying to build a parser for lambda expressions. I have implemented a capture-avoiding substitution using the algorithm below ($e[d/x]$ means replace $x$ by $d$ in $e$)
$x[d/x] = d$
$y[d/x] = y$ ...
- 11
0
votes
1
answer
48
views
How does one define transcendental numbers (such as Pi) in theory of general recursive functions
On a turing machine and in the lambda calculus one can define transcendental numbers such as Pi, the golden ratio, etc.
These are computatible functions with 0-arity that never terminate.
In the ...
- 141
-1
votes
1
answer
84
views
Equivalence between Lambda Calculus [Church] and Computable Partial Functions [Godel]
In order to show that Lambda calculus and Turing machines are equivalent it is sufficient to show that you can simulate one in the other [both ways].
We can observe it in action. Can one do the same ...
- 141
1
vote
1
answer
59
views
How does GHC insert type abstraction/application under the RankNTypes extension
I'm developing a functional programming language that offers Rank-n polymorphism. Like Haskell I don't want types to appear at the term level, but I have no idea to insert type abstraction and type ...
- 13
0
votes
2
answers
53
views
Lambda body reduction in Lambda calculus
I'm studying lambda calculus with De Bruijn indexes, and have these functions.
$$
zero := (\lambda\lambda.1)\\
succ := (\lambda\lambda\lambda.2 (3 2) 1)
$$
Now I want an algorithm to reduce $succ\ ...
- 243
1
vote
1
answer
61
views
Must the evaluation strategy for a language be specified in order to apply the Church-Rosser Theorem?
The Church-Rosser Theorem [0] states that the Lambda Calculus (LC) is
confluent: between a source expression S and target expression T, the
latter in normal form, for any given P, a sequence of ...
- 39
2
votes
1
answer
65
views
Is there a hierarchy of computational expressivity that is sensitive to evaluation strategies?
Various computational hierarchies describes the relative
expressivity of different classes of languages, machines, or other
models of computing, with the classic progression for Automata Theory
[0] ...
- 39
1
vote
1
answer
58
views
What are distinguishable terms in Bohm theorem?
I have just started to study "Lambda-Calculus and Combinators, an Introduction" by Roger Hindley.
There is a formulation of B ̈ohm’s theorem that I can not understand.
$M$ and $N$ are terms ...
- 299
2
votes
1
answer
159
views
Formal language rewrite rules: strange notation
I'm reading "Program=Proof" by Samuel Mimram, and they use a notation for defining a formal language that I'm not familiar with.
Here is how "Program=Proof" defines a formal ...
- 184
0
votes
1
answer
54
views
Are there syntactic conditions on divergent $\lambda$-terms?
Probably the most famous example of a divergent term (ie, one which admits infinitely many $\beta$-reductions) in the $\lambda$-calculus is the Y combinator
$$ Y = \lambda f. (\lambda x. f(xx)) (\...
- 133
2
votes
2
answers
79
views
What is the lower bound on retrieving an item in a collection if no arrays(Random access memory) are allowed?
I know that retrieving an item in a collection can be done in $O(1)$ time(on average) using hash tables. I would like to know if there is an algorithm that could be as performance without using arrays....
- 235
2
votes
1
answer
63
views
Turing Machine for the Language $L=\{(a^n)b(a^n)b(a^n) | n\geq0\}$
Turing Machine for the Language $L=\{(a^n)b(a^n)b(a^n) | n\geq0\}$
Here is what I have tried:
1. Starting State
Read $a$, Write $x$, Move Right, Go To 2
Read $x$, Write $x$, Move Right, Go To 1
Read <...
- 135
2
votes
2
answers
90
views
Why do combinators look this way?
Out of curiosity, why do combinators look this way? For example, why is $K = \lambda x y \to x$ and why is it called $K$? Why is it not $\lambda x y f m \to f m x$? These are just arbitrary letters, I ...
- 121