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
2 votes
2 answers
61 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....
user avatar
  • 235
2 votes
1 answer
51 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 <...
user avatar
  • 121
2 votes
2 answers
70 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 ...
user avatar
2 votes
1 answer
67 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 ...
user avatar
  • 21
0 votes
0 answers
51 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 (...
user avatar
1 vote
1 answer
73 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 ...
user avatar
  • 35
0 votes
0 answers
24 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/...
user avatar
  • 555
0 votes
2 answers
110 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 ...
user avatar
  • 459
1 vote
2 answers
69 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₁...
user avatar
  • 5,002
2 votes
2 answers
53 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 ...
user avatar
  • 5,002
1 vote
1 answer
78 views

Call by name, lambda calculs. Multiplication

How to multiply in CBN strategy? ...
user avatar
1 vote
1 answer
87 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 ...
user avatar
  • 13
4 votes
1 answer
534 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: ...
user avatar
  • 43
2 votes
0 answers
75 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 ...
user avatar
2 votes
1 answer
41 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 ...
user avatar
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, ...
user avatar
  • 119
1 vote
0 answers
32 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? ...
user avatar
  • 386
2 votes
0 answers
24 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 ...
user avatar
  • 197
3 votes
1 answer
115 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 ...
user avatar
  • 63
3 votes
0 answers
42 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 ...
user avatar
3 votes
0 answers
63 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 ...
user avatar
2 votes
0 answers
48 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.
user avatar
  • 121
0 votes
0 answers
32 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 ...
user avatar
  • 219
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: ...
user avatar
1 vote
0 answers
45 views

Delayed "let" in SICP

In section 3.5.4 , i saw this block: ...
user avatar
0 votes
1 answer
294 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 ...
user avatar
  • 111
1 vote
1 answer
83 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 ...
user avatar
0 votes
1 answer
34 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 ...
user avatar
2 votes
1 answer
76 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 ...
user avatar
  • 145
2 votes
2 answers
137 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: ...
user avatar
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 ...
user avatar
3 votes
0 answers
45 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))(...
user avatar
  • 41
5 votes
0 answers
99 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$-...
user avatar
2 votes
1 answer
36 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}$
user avatar
  • 21
4 votes
1 answer
93 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 ...
user avatar
  • 2,196
0 votes
0 answers
48 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 ...
user avatar
  • 231
3 votes
1 answer
64 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/...
user avatar
2 votes
1 answer
64 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 ...
user avatar
  • 163
3 votes
2 answers
311 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 ...
user avatar
4 votes
1 answer
61 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 \...
user avatar
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?
user avatar
2 votes
1 answer
70 views

Computation equivalence of functional and procedural programming

I'm really interested in the idea of functional programming, it seems like a very modular way of doings things. I've seen some suggestion that functional programming is just as powerful as procedural ...
user avatar
2 votes
0 answers
70 views

Church Numerals represented as a List?

Afternoon All, Perhaps an easy one for many, but am new to Lambda calculus: Is the below list, Ni, a representation of the Church numerals? I think it is but how do I prove it...if not, what is it...? ...
user avatar
1 vote
1 answer
205 views

λ -terms that correspond to Haskell functions

Evening All I already have a "grasp" of haskell (not terrible, about 6 month experience) and am trying to learn the fundamentals that sit behind it, thus am now turning my attention to ...
user avatar
2 votes
1 answer
125 views

Show that term cons works by showing all beta reductions

I'm new to functional programming. So the terms cons appends an element to the front of the list. Where cons ≜ λx:λl:λc:λn: c x (l c n). How should I go about proving that cons works correctly using ...
user avatar
1 vote
1 answer
42 views

Category Set language using simply typed lambda calculus

I am currently self learning Category Theory and Simply typed lambda calculus (STLC). For learning purposes, I have implemented an STLC interpreter as given in Types and Programming Languages book ...
user avatar
  • 11
0 votes
0 answers
30 views

Is type unification a kind of search for alpha equivalence?

I was reading about type unification and it moves through of substitution of variables. To me it looks like a search for an alpha equivalence... I mean, two types are unifiable if they are alpha ...
user avatar
  • 219
2 votes
1 answer
39 views

Why $((+ 1) ((+ 1) 1))$ is not a $\delta-$redex?

I was reading http://barrywatson.se/lsi/lsi_delta_reduction.html, where ((+ 1) 2) →δ 3 is a δ-reduction. ((+ 1) ((+ 1) 1)) is a not a δ-redex. Wouldn't $((+ 1) ((...
user avatar
  • 219
1 vote
1 answer
70 views

Beta reduction of S combinator in pure lambda calculus

S is defined as S x y z = x z (y z) This suggest that (y z) should be evaluated just after ...
user avatar
  • 219
0 votes
1 answer
125 views

Fixed Point Combinator Turing proof

I have to proof that Turing's combinator is a fixed point operator, but I can't get it. I tried this: \begin{align*} Vg &= (UU)g = ((\lambda f.\lambda x.x(ffx)) (\lambda f.\lambda x.x(ffx)))g =...
user avatar
  • 125

1
2 3 4 5
11