Questions tagged [lambda-calculus]

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

Filter by
Sorted by
Tagged with
6
votes
0answers
73 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
2
votes
1answer
52 views

“not provable”, what does this to do with unification?

I found one interesting point in nominal unification. Just after proposition 2.16 of Nominal Unification by Urban, Pitts, and Gabbay, it said the following, which I found confusing: For non-ground ...
9
votes
0answers
126 views

Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection

Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category. I was wondering if in such context it is ...
4
votes
1answer
281 views

Lambda Calculus in Rewriting systems

How to do or implement Lambda Calculus in a Rewriting systems? Rewriting systems are Turing complete. But I can't figure out how to do lambda calculus or functions with them.
2
votes
1answer
127 views

Is this a valid representation of a function in Lambda Calculus?

Let's say I want to define a function: This function multiplies an input by two, adds one to this integer, then divides it by two in that order. f represents the multiplication, g represents the ...
5
votes
1answer
141 views

Functorial type constructors in System F

I have come across the claim that all basic data types in System F, such as Bool, Nat, and List(U), can be expressed in the form $\forall \alpha (((T\alpha \rightarrow \alpha) \rightarrow \alpha)$, ...
1
vote
1answer
455 views

What can you do with lambda calculus if you aren't allowed parentheses?

Is there a concise/existing way to denote the expressive power of "lambda calc without using parentheses/tree-of-expressions/application-order-restructuring anywhere"? Can you do without them/...
5
votes
2answers
150 views

Nominal unification: How this lemma is proved?

I was reading nominal unification paper. I could not understand the proof of a lemma. The paper is here nominal unification. The lemma is following. $\sigma$ is a substitution, $\pi$ is a permutation ...
4
votes
1answer
363 views

How to prove equivalence relation in this case?

I am working on $\lambda$-terms and trying to prove the $=$ is an equivalence relation on $\lambda$-terms. My problem is proving reflexive relation. $\frac{}{\theta \vdash x = x}$ $\frac{ \theta,x \#...
3
votes
1answer
81 views

Term of System F whose type-erasure is $2(2)$

If $2$ is the Church numeral $\lambda fx. f(f(x))$, then is there a closed term $t$ of System F of type $\forall \alpha ((\alpha \to \alpha) \to (\alpha \to \alpha))$ such that the type-erasure of $t$ ...
1
vote
1answer
29 views

Example of typed lambda term with recomputed argument

What is an example of a typed lambda term $\lambda x.\phi : A \to B$ and a term $a : A$ such that, when $\beta$-reducing the term $(\lambda x.\phi)(a)$, the argument $a$ must be repeated/recomputed ...
4
votes
2answers
808 views

What is a quotient structure?

I was reading a paper here, and it mentioned "quotient structure" in the following sentence (third page, second paragraph of the paper) In order to obtain a representation of terms truly isomorphic ...
0
votes
1answer
72 views

Class of languages that are equivalent to the lambda calculus

It is well known that all computable functions can be expressed as terms of the lambda calculus and computed according to its rules. It is also more or less obvious that many classical formal ...
1
vote
2answers
63 views

Any notions of operations in basic postulates of lambda calculus

I am learning Lambda Calculus from the book by Hindley and Seldin . They start the formal postulation of lambda calculus as follow : (a) all variables and atomic constants are λ-terms (called atoms);...
0
votes
1answer
79 views

$\lambda x. \lambda x.x$ vs $\lambda y. \lambda x.x$

Several times, I saw $\lambda$-terms such as $\lambda x. \lambda x.x$, where $x$ is bound by the inner lambda, which I agree. why not just write it as $\lambda y. \lambda x.x$, so it is clear and ...
2
votes
1answer
263 views

Basic notation in lambda calculus

I have started learning lambda calculus from the book by Hindley and Seldin. It brought up the concept with the function $x-y$, first as a function of $x$ and then as a function of $y$. In a way, it ...
2
votes
2answers
259 views

A basic question about recursive computation

I was going through the following paper: http://www-formal.stanford.edu/jmc/recursive.pdf In the last part of the second section (at the end of page 7) he speaks about the inadequacy of lambda notion ...
1
vote
1answer
293 views

What makes data flow analysis higher level than control flow analysis?

I feel understanding why data flow is higher level than control flow is key to writing good code (and convincing others during code reviews). I find this repeatedly when arguing why my functional ...
2
votes
1answer
124 views

Difference between $\beta$-contracts and $\beta$-reduces in Hindley

I brought the book Lambda-Calculus and Combinators: An Introduction by J. Roger Hindley and the author explains what is $\beta$-reduction. Now there is a difference between $\beta$-contracts and $\...
2
votes
1answer
2k views

Difference between beta reduction and substitution

I can not see the difference between beta reduction and substitution. For example: (+ x 1) [x -> 2] Here I can do the substitution, replace the variable x ...
1
vote
1answer
97 views

Lambda calculus application [closed]

I have a function application: E1 E2 Can someone please show me an example, how to execute function?
2
votes
1answer
40 views

Why it converts to T

The AND function in the lambda is: and = (λ a. λ b. a b F) I have following expression: and T T then the result will ...
2
votes
2answers
131 views

Problem with Church numerals evaluation

I am trying to understand Church's Numerals for 4: $$4 = \lambda f.\, \lambda x.\, f f f f x\,.$$ This will be evaluated in the following order: $$\lambda f.\, \lambda x.\, (f (f (f (f x) ) ) )\,.$$...
2
votes
2answers
379 views

What is the point of this lambda expression?

Let's take this lambda expression : $\lambda\:x \:\ast\:x\:2$ that "computes" x * 2. From what I understand, $\ast$ is a constant operator, but since its nothing ...
7
votes
1answer
391 views

Intuitive explanation of neutral / normal form in lambda calculus

It is possible to distinguish Normal terms which don't contain beta redex as a sub-expression, from others like so ...
4
votes
2answers
199 views

What's the difference between the rank and the degree of a type function?

1 Context Near pg. 184 of Lambda Calculus and Combinators, the author is discussing the theory of dependent types. In particular, we are extending the lambda calculus to look at terms of form $$ \Pi ...
1
vote
1answer
285 views

how to understand the occurrences of free variables?

I am thinking that many example only takes free variable with one occurrence, such as $(\lambda x.x )y$ where $y$ is free. can we say $y y $ is a $\lambda$-term and two $y$ are same free variable? I ...
6
votes
0answers
863 views

Barendregt's Variable Convention: what does it mean?

Barendregt's Variable Convention: If $M_1,...,M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free ...
0
votes
1answer
384 views

Order of argument application in lambda calculus

I encountered the following exercise in a textbook about logic: $\lambda x \lambda Y(Y(x))(j)(M)$ It seems that the expected result from the textbook should be $M(j)$, since there were some type ...
1
vote
1answer
171 views

Comparison Procedure in Robinson's Unification Algorithm

I'm studying the Principal Type (PT) Algorithm in Basic Simple Type Theory by J. Roger Hindley. One step to find the PT of a term is the Unification of types. The Robinson's Unification Algorithm uses ...
1
vote
1answer
45 views

Connecting The Informal and Formal Definitions of Decidable With Each Other

From pg. 64 of Lambda Calculus and Combinators, the author formally and informally defines the notion of "decidability": 1 Formal Definition Definition 5.4 A pair of sets $\mathcal{A}$, $\mathcal{...
6
votes
2answers
1k views

Why are combinators important in lambda calculus?

I just recently learned a little about the lambda calculus, from the brief intro in the text Programming Language Pragmatics and this outstanding 4-video sequence from Adam Doupé. Basically I learned ...
1
vote
1answer
66 views

Trouble Replicating Proof of The Lambda Calculus Fixed Point Theorem

From pg. 35 of Lambda Calculus and Combinators An Introduction: Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0$, the equation $$ xy_1 \ldots y_n = Z $$ can be solved ...
8
votes
1answer
528 views

Recursive type encoding on System F (and other pure type systems)

I am studying pure type systems, particularly the calculus of constructions, and trying to use an encoding for recursive types on it, which, according to Philip Wadler, is possible. As an example, I'm ...
1
vote
0answers
22 views

How to interpret scoped variables next to each other within Lambda Terms and CL-terms?

In both the lambda calculus ($\lambda$-calculus) and Combinatory Logic (CL), we have the notion of function application. For example: \begin{array} & \left( \lambda x . x \right) y = y & \...
2
votes
1answer
50 views

Trouble Understanding a Remark about Beta-Reduction in the Lambda Calculus

From page 15 of Lambda Calculus and Combinators an Introduction: Note 1.34 If $M \equiv aM_1 \ldots M_n$ where $a$ is an atom, and $M \triangleright_\beta N$, then $N$ must have form $$ N \...
3
votes
1answer
85 views

Understanding A Recursive Definition of CL-Terms in Combinatory Logic

From page 26 of Lambda-Calculus and Combinators: Definition 2.18 (Abstraction) For every CL-term $M$ and every variable $x$, a CL-term called $[x].M$ is defined by induction on $M$, thus: (a)...
2
votes
1answer
106 views

Is there a correspondence between the syntaxes and the type systems of programming languages?

I was reading the first chapter of Robert Harper's Practical Foundations for Programming Languages in which it introduced abstract binding trees, aka abt. It seems pretty like typed lambda calculus. ...
2
votes
1answer
200 views

ground terms in logic and $\lambda$-calculus?

What are the differences of ground terms in first-order logic and higher-order logic? I found on the Wikipedia: "In mathematical logic, a ground term of a formal system is a term that does not ...
5
votes
2answers
105 views

Why is the word “calculus” used to describe systems of logic and computation?

Why is the word "calculus" used in this context? The reason I ask is because these usages of "calculus" seem unrelated to the far more popular use of "calculus" in "differential calculus" and "...
4
votes
1answer
1k views

What is the difference between strong normalization and weak normalization in the context of rewrite systems?

In the context of rewriting systems, how does strong normalization differ from weak normalization?
2
votes
1answer
203 views

How is this expression a valid lambda expression?

Can you explain how this expression follows the grammar of the lambda calculus? $$\lambda x.x((\lambda y.yy)x)x = λx.x(xx)x$$ I am not sure why we have the parentheses following the $.x$ (on both ...
9
votes
1answer
213 views

What is a super universe?

I'm reading this well-known paper On Universes in Type Theory. At first I expected something similar to Setω in Agda, but it turns out that it's even something more ...
3
votes
1answer
2k views

Lambda calculus lists construction explanation

I have the following notes that introduce how lambda calculus handles lists. They go as follows: A list is something we can match on and deconstruct if it is not empty: ...
4
votes
1answer
120 views

how to prove the following is a bijection?

I have a translation function which translates $\lambda$-terms to another representation let me call it $G_\lambda$, as follows. $\chi(x)$ $=$ $ X^2$ if $ x \notin \Gamma$ $\...
3
votes
0answers
164 views

$\lambda$-terms equal modulo $\alpha$-renaming, is this an equivalence relation?

Want to clarify few things. It is said that two $\lambda$-terms are equal up to renaming of bound variables, such as $\lambda x.x$ equals $\lambda y.y$, so I think it is a relation actually, about ...
19
votes
7answers
3k views

Lambda calculus didn't seem abstract. And I can't see the point of it

The underlying question: What does lambda calculus do for us that we can't do with the basic function properties and notation generally learned in middle school algebra? First of all, what does ...
4
votes
1answer
77 views

Definition of integers needs explaining

Zero and one are defined by the successor function. $$ \begin{align*} &0 ≡ λsz.z \\ &1 ≡ λsz.s(z) \end{align*} $$ But why? $λsz.z$ is irreducible to a value. If I call this function on some ...
4
votes
1answer
99 views

what is weak extensionality in $\lambda$-calculus?

I was reading the book lambda calculi , encountered an equality theory called "the rule of weak extensionality", which is shown as follows. $\frac{M \, = \, N}{\lambda x.M \, = \, \lambda x.N}$ Yes,...
1
vote
1answer
113 views

Proving using Beta Reductions (Lambda Calculus)

I am working on proving something by using Lambda Calculus and Beta Reductions, and I was following along a tutorial on another problem and attempted to carry over the knowledge onto a different ...

1
3 4
5
6 7
9