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
0 votes
0 answers
18 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 emulate one in the other [both ways]. How does one emulate lambda calculus in recursion ...
  • 111
1 vote
1 answer
28 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
38 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
0 votes
0 answers
58 views

How to go about solving this induction?

The terms Lm and L′m for each natural number m are defined as follows. (Note that n and c are variables whereas m stands for a number or its Church encoding.) ...
user avatar
2 votes
1 answer
38 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 ...
  • 41
2 votes
1 answer
41 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] ...
  • 41
0 votes
0 answers
27 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 ...
  • 287
2 votes
1 answer
125 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 ...
0 votes
1 answer
40 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
70 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
57 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 <...
  • 133
2 votes
2 answers
81 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 ...
2 votes
1 answer
122 views

Addition in Lambda calculus

Found this term for a supposed 'adder' in lambda calculus. λabcd.ac(bcd) Although I know about alpha-conversion and beta-reduction and all that stuff, I don't know ...
  • 21
1 vote
0 answers
69 views

What actually IS lambda calculus and how do I actually apply it?

Trying to wrap my head around lambda calculus but am really clueless right now. First of all, I'm really confused WHAT it's actually supposed to be. I've found these definitions: Lambda calculus (...
  • 19
2 votes
1 answer
91 views

Why use the Y combinator for recursion?

The Y combinator is defined as $$Y=\lambda f.(\lambda x. f (x x))(\lambda x. f (x x))$$ It has the following useful property: $$Y g = g (Y g)$$ for some expression $g$. It can be easily used to ...
  • 55
0 votes
0 answers
25 views

Two CPS translations for CBV lambda calculus

I am looking for the CPS translation for CBV evaluation order in lambda calculus, and I have found the two following versions of the translation. The first is given there: https://www.cs.cornell.edu/...
  • 565
0 votes
2 answers
118 views

Why we can not define factorial in lambda calculus

I came across factorial semantics using lambda calculus: $$fact = \lambda n. if(iszero~n) (1) (mult~n(fact(pred~n)))$$ I am not sure why the above does not make sense. Why we just can not keep ...
  • 459
1 vote
2 answers
84 views

Free variables as defined in TAPL seems wrong

In "Types and Programming Languages" by Benjamin C. Pierce (WorldCat) 5.3.2 Definition: The set of free variables of a term t, written FV(t), is defined as follows: FV(x) = {x} FV(λx.t₁...
  • 5,052
3 votes
2 answers
62 views

What does "lambda terms modulo convertibility" mean?

In "The Lambda Calculus - Its Syntax and Semantics" by H.P. Barendregt (WorldCat) is this statement, the first sentence of chapter 2 after the introduction chapter, so in a way this sets the ...
  • 5,052
1 vote
1 answer
86 views

Call by name, lambda calculs. Multiplication

How to multiply in CBN strategy? ...
1 vote
1 answer
94 views

define the head expressions

List $[E1,E2,...,Ek]$ in lambda expression can write as $$λc.λn.cE1(cE2(...(cEkn)...))$$ Based on this, how to define head and ...
  • 13
4 votes
1 answer
540 views

How could you encode such a function in lambda calculus?

I just read the definition of lambda calculus. Apparently it's Turing complete, but I tried writing a very simple function and I couldn't: ...
  • 43
2 votes
0 answers
100 views

What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?

I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
2 votes
1 answer
72 views

Is there a way to represent multi-dimensional arrays in lambda calculus?

I am currently studying lambda calculus, and would like to represent an array that accepts multiple dimensions. I still haven't figured out how to implement uni-dimensional arrays though. I have found ...
10 votes
4 answers
4k views

What are some interesting/important Programming Language Concepts I could teach myself in the coming semester?

I’m a CS senior with and Individual Study period this coming semester, and I’ve decided I’d like to learn more about Programming Language Concepts. More specifically, different programming paradigms, ...
  • 119
1 vote
0 answers
45 views

CEK machine vs SECD machine

What are the differences between the CEK machine and the modern variant of the SECD machine (which combines stack and dump) from the point of view of performance, memory efficiency, and other factors? ...
  • 386
2 votes
0 answers
25 views

Are there any references for this theorem of Lercher?

Let $\Delta = \lambda x.(x)x$ and consider $\Omega = (\Delta)\Delta$. Then $\Omega$ is exactly the only $\lambda$-term of the form $(\lambda x.t)v$ such that $(\lambda x.t)v=t\{v\ /\ x\}$. Does ...
  • 199
3 votes
1 answer
120 views

How, if possible, can we efficiently compute with lazy data structures in 𝜆-calculus?

In Haskell, we can use the following code to define fibonacci numbers, fibs = 1 : 1 : zipWith (+) fibs (tail fibs) And its time complexity is linear. I cannot find ...
  • 63
3 votes
0 answers
53 views

Equivalence between $\lambda$-calculus and recursive functions

I have two related questions: Do you know of any good reference to the recursive function / lambda-calculus equivalence in terms of computability, including proofs? Do you know of any reference to ...
3 votes
0 answers
71 views

Lemma relating variable substitution to de Bruijn substitution

Notation: Let $t$ and $u$ be terms in the $\lambda$-calculus, and $x$ be a variable name. Let $[x\mapsto u]t$ be the substitution in $t$ of free variable $x$ for the term $u$. Specifically, I'm ...
2 votes
0 answers
52 views

What are the fixed-points of the Y combinator?

Since the Y combinator itself is a function (albeit a higher-order one), I was wondering what the fixed-points of Y itself are.
  • 121
0 votes
0 answers
39 views

How to verify/proof that my lambda calculus is correct?

I was reading about proof assistants, formal verification etc, also I have a lambda calculus implementation. My question is: Is it possible to prove that my implementation is correct? In fact I have ...
  • 243
0 votes
0 answers
33 views

Lambda Calculus: Re-Ordering Arguments

Given any multivariable expression in Lambda Calculus (LC), e.g. for an arbitrary LC expression "op" for some non-commutative operation: ...
1 vote
0 answers
47 views

Delayed "let" in SICP

In section 3.5.4 , i saw this block: ...
0 votes
1 answer
301 views

What benefits are obtained by allowing the occurrence of free variables and open terms in lambda calculus?

Because of the existence of free variables in lambda calculus, the evaluation of open terms (at least as outlined here) is more complicated relative to the evaluation of closed terms since the ...
  • 111
1 vote
1 answer
99 views

Proving intuitionistic tautologies in Agda

I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law $$ ((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B $$ I ...
0 votes
1 answer
35 views

On lambda calculus notation: FGa

If we've got this expression: FGa where F and G are functions (as well as a, of course; but let's treat a as a constant). It must be understood that: first apply F taking G as input; then apply the ...
2 votes
1 answer
96 views

Can the Y-combinator really terminate?

My understanding of the Y-combinator is that it never terminates (Yg = g(Yg)). Its termination is only decided externally to the $\lambda$ specification when it has ...
  • 145
2 votes
2 answers
146 views

Is this definition of $\alpha$-equivalence correct?

I want to extend $\alpha$-equivalence to cover substitution. That is, I will implement runSubst_Term : Subst -> Tm -> Tm and prove: ...
2 votes
0 answers
36 views

Is there a functional programming language with inherent change propagation?

Change propagation in programming environments is an add-on at the framework level such as React. There was a lot of work on dataflow virtual machines in the wake of Backus's Turing Award Lecture on ...
3 votes
0 answers
53 views

Equality of lambda terms which do not have normal form

In the context of lambda calculus, how should one prove $\beta$-equality of terms that do not have normal form? In particular, how to prove that these are different combinators: $$ Y = λf.(λx.f(xx))(...
  • 51
5 votes
0 answers
101 views

Is α-renaming necessary for STLC?

Consider the following in untyped lambda calculus ( \ x. x x ) ( \ g. \ f. g f ) Even though each variable is uniquely named reducing this will require an $\alpha$-...
2 votes
1 answer
39 views

Raising to the T in machine learning

What does it mean when in a machine learning paper there is $(arg)^{T}$, what does the T does to an arg in this 3b1b video on neural networks he puts the: $(w^{l-1})^{T}$
  • 21
4 votes
1 answer
101 views

Proving program termination in the $\lambda$-calculus

Turing's Checking a large routine: Finally the checker has to verify that the process comes to an end. Here again he should be assisted by the programmer giving a further definite assertion to be ...
  • 2,230
0 votes
0 answers
49 views

Association rules during execution in lambda calculus

I learned that expressions are left associative while abstraction are right associative, however, while solving some examples i faced this problem. Succ 3 Succ 2 when i applied left associativety i ...
  • 229
3 votes
1 answer
69 views

How is `y λx.x y` parsed using the standard pure untyped lambda calculus conventions?

How would the following term in the pure untyped lambda calculus be parsed: y λx.x y The relevant conventions listed on https://en.wikipedia.org/wiki/...
2 votes
1 answer
68 views

Simplify the definition of substitution in Lamdba calculus

Substitution in untyped Lambda calculus is complicated by variable capture. Can this boring technical complication be entirely avoided by some restriction on the standard formation rules? Something ...
  • 163
3 votes
2 answers
337 views

What is congruence in lambda-calculus

I see a lot of lecture notes where they use the term "congruence" (ex: congruence relation) or deriving usages such as "the expression e is alpha-congruent to e2". Could someone ...
4 votes
1 answer
62 views

Proving equivalence of two substitutions by induction

I'm trying to prove the following reduction: $$ t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\} $$ under the following assumptions: $x \neq y$ $x$ is not a free variable of $v$ (in symbols, $x \...
1 vote
0 answers
38 views

Can a lambda expression be beta-equal to beta-normal forms?

Given a Lambda Expression Term T can it be beta-equal to two different Lambda Terms T1 and T2, both T1 and T2 are in beta-normal form?

1
2 3 4 5
11