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
1
vote
0answers
25 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.
0
votes
0answers
23 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 ...
0
votes
0answers
26 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
0answers
37 views

Delayed “let” in SICP

In section 3.5.4 , i saw this block: ...
0
votes
1answer
244 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 ...
1
vote
1answer
41 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
1answer
26 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
1answer
51 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 ...
2
votes
2answers
104 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
0answers
26 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
0answers
35 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))(...
5
votes
0answers
78 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
1answer
31 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}$
3
votes
1answer
50 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 ...
0
votes
0answers
42 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 ...
0
votes
0answers
41 views

Is there a standard way to do Debrujin indices for an uncurried language?

With Debrujin indices, variable names are replaced with numbers that indicate which function binds them. This works fine if each function only binds one variable, but what if one's language is not ...
2
votes
1answer
46 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
1answer
52 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 ...
3
votes
2answers
245 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
1answer
54 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
0answers
35 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?
2
votes
1answer
58 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 ...
2
votes
0answers
54 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...? ...
1
vote
1answer
112 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 ...
2
votes
1answer
85 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 ...
1
vote
1answer
31 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 ...
0
votes
0answers
27 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 ...
2
votes
1answer
27 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) ((...
1
vote
1answer
39 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 ...
0
votes
0answers
37 views

What kind of automaton recognizes closed terms of the lambda calculus?

There seems to be an interesting model of computation involved in determining whether a term from some programming language has any free variables. It's a tree traversal that seems almost like the ...
0
votes
1answer
43 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 =...
3
votes
1answer
84 views

What is the diference between $\lambda x.1$ and $1$?

I know that I can $(\lambda x.1) 0 \rhd_\beta 1$. This is the constant 1, but can I contract it automatically? I mean, is $1$ the normal form of $(\lambda x.1)$? It seems reasonable to do it but when ...
0
votes
1answer
49 views

Is (λx.FV(A)) and (λx.FV(B)) β-equivalent?

Does free variables have some meaning in lambda calculus? If I follow this β-reduction ...
1
vote
0answers
30 views

Other encodings of the natural numbers that are not the Church encoding or the Scott encoding

Are there other encodings of the natural numbers in the untyped lambda calculus which are neither the Church encoding nor the Scott encoding?
1
vote
0answers
20 views

Imposing sortal restrictions on functions in the untyped lambda calculus

In the simply typed lambda calculus if we have an addition operator, $+ : n \to n \to n$, its typing imposes that we can only combine it with something of a given type. So if $n$ is the type of ...
3
votes
1answer
87 views

The difference between $\beta$-reduction and $let$

These are the reduction rules associated with $\beta$ reduction and $let$: $$(\lambda x. e_2) e_1 \to_{\beta} e_2 [e_1 / x]$$ $$let \,x = e_1 \textit{ in }e_2 \to e_2 [e_1/x]$$ These reduction rules ...
0
votes
2answers
134 views

Why should I care about lambda calculus

I am a programmer by hobby. I stumbled upon lambda calculus from Kevlin Henney's talk lambdas to the slaughter and I was sold! It was an interesting new way of thinking that's entirely different than ...
2
votes
1answer
30 views

How would you model Rust procedural macros?

In Rust programming language one can write a compiler extension function that works on abstract syntax tree, effectively modifying source code before it gets converted into machine instructions. In ...
5
votes
0answers
179 views

Normalization-by-evaluation for untyped lambda calculus which results in 𝛽𝜂-normal form

Usual NbE algorithms for untyped lambda calculus, which use (P)HOAS to embed terms to a host language constructs, results in a beta-normal form of a terms. Is there algorithms to (efficiently) exploit ...
4
votes
2answers
217 views

Sequencing or continuation-passing in pure lambda-calculus

I am trying to solve the following exercise given here. Consider the following number representation. How to define the addition? ...
0
votes
1answer
39 views

Lambda calculus simplification excercise

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. (λx.λy.yx)z (λw.w) I am lost with this. if anyone could lead me in ...
2
votes
1answer
117 views

Is the term $(\lambda x.x)(y y)$ a normal form in call-by-value reduction strategy?

I am learning λ-calculus and I have some confusion about it. Is the term $(\lambda x.x)(y y)$ a normal form in call by value reduction strategy? (where $y$ is a free variable) From the wikipedia, it ...
5
votes
0answers
115 views

What's the internal language of the opposite of a Cartesian closed category?

I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories. What's the internal language of the opposite type of category? The rules dual to currying and ...
1
vote
0answers
49 views

How to write “∀x.F(x)” for “F(x)=λx.Φ(x)” in one expression (sequel from question about “∀(λφ. (φ x m→ φ y))”?

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context. So - I have anonymous Boolean-valued ...
4
votes
3answers
137 views

Can lists be defined in a special way so that they contain things of different type?

In https://www.seas.harvard.edu/courses/cs152/2019sp/lectures/lec18-monads.pdf it is written that A type $\tau$ list is the type of lists with elements of type $\tau$ Why must a list contain ...
2
votes
1answer
314 views

How to understand quantifier without predication “ ∀(λφ. (φ x m→ φ y))”?

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
2
votes
1answer
131 views

Creating a large tuple from smaller tuples via a monad or applicative

Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term $\lambda x_{\beta}. \;(x, \, ...
3
votes
0answers
92 views

(Co)-monads and terminating implementations

The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).' Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
3
votes
1answer
259 views

The meaning and relevance of the locution ''no terminating implementation'' in type theory

In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that There is no terminating ...
1
vote
0answers
26 views

Constructing a monad via type synonyms of a particular kind

We can define a reader/environment monad on the simply-typed lambda calculus, using the following three equations, where $r$ is some fixed type, $\alpha$ is any type (I subscript some terms with their ...

1
2 3 4 5
10