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
1answer
20 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) ((...
0
votes
1answer
25 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
23 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
20 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 =...
1
vote
1answer
73 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
42 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
21 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
19 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
78 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
85 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
20 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
168 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
202 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
33 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
0answers
43 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
103 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
47 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
125 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
305 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 ...
1
vote
1answer
101 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
89 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
255 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
vote
2answers
79 views

Lambda Calculus Conversion

How can I take a Haskell data type or function (eg fold, list, String, zip) and convert or translate it to a lambda calculus abstraction? Example: If sum computes a sum of all elements in a list, and :...
2
votes
0answers
48 views

Inhabitation of STLC is in PSPACE

Urzyczyn: Inhabitation in Typed Lambda-Calculi (A syntactic approach) gives a proof that STLC inhabitation problem is in PSPACE (section 2, lemma 1). I don't understand certain aspects of the proof: ...
2
votes
1answer
49 views

Tried to derive the Z combinator and instead derived another

I was working to derive the Z-Combinator by starting with the factorial function and ended up deriving a different fixed-point combinator. What did I derive? Did I make a subtle mistake? Here are the ...
3
votes
2answers
121 views

alpha equivalence of lambda calculus

I am pretty new in λ calculus. And I am now trying to understand Alpha equivalence. Basically can I think it in this way: as long as I make sure all the bound variables and their corresponding ...
3
votes
0answers
66 views

Understanding $\lambda \mu$-calculus in more programming way

I am learning $\lambda \mu$-calculus (self-study). I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
2
votes
1answer
42 views

Lambda calculus without free variables is as strong as lambda calculus?

First question: How would one prove that by removing free (unbound) variables from lambda calculus, and allowing only bound variables, its power is not reduced (it is still Turing-complete) ? Second ...
2
votes
1answer
77 views

What does Lambda Calculus teach us about data?

In Lambda Calculus, the distinction between data and code doesn't seem to exist. Is there something fundamental about this, or purely Lambda Calculus's thing? Some context: as a software developer, I ...
2
votes
3answers
91 views

Uncurrying and Polymorphism

How do we uncurry functions when they are polymorphic? For example, is it possible to uncurry the following types? If so what is the uncurried type? $\forall X. X \rightarrow int \rightarrow X$ ? $...
1
vote
0answers
45 views

Lambda calculus and runtime inspection of the term

This is possibly related to reflection and quoting but I don't want to assume anything beforehand. Here is my requirement. My typed lambda calculus (Curry style) is a simpler variant of Calculus of ...
0
votes
0answers
29 views

How does this dependently-typed boolean elimination function work?

In the companion code to A Tutorial Implementation of a Dependently Typed Lambda Calculus - prelude.lp - there is a rather intimidating definition of a ...
3
votes
1answer
71 views

What are Contexts in Lambda Calculus?

What is a Context? Is it like a scope in C? Does it have a start and an end? Can contexts contain other contexts? I see Contexts being used in lambda calculi type system rules, but I don't understand ...
2
votes
2answers
63 views

Tightening application rules for STLC

The syntax STLC is usually written: $e ::= x |\lambda x : \tau . e|(e \space e)|c$ However, the application rule appears to accept all expressions on the left hand side. Shouldn't the application ...
2
votes
0answers
20 views

Reducing Kleene's predecessor for Church numerals

I am trying to "reinvent" Kleene's predecessor myself. The following code snippet should be self-explanatory. The idea is to make a 2-tuple and count up from zero, i.e. ...
5
votes
0answers
128 views

Where is typed lambda calculus on the Chomsky hiererchy?

The functions definable in untyped lambda calculus are the computable functions, for which it is in turn possible to define equivalences to the concepts of Turing machines, recursive enumerability and ...
0
votes
0answers
17 views

Does there exist a way, within Lambda Calculus, to discover if two free variables are the same?

Using Church's $\lambda x.(\lambda y.y))$ as false and $\lambda x.(\lambda y.x))$ as true, and given two free variables $g$ and $h$: Could there exist a function $eq?$ such that $(eq?\ g\ h)$ is ...
0
votes
1answer
55 views

lambda calculus beta reductions: ((((lambda f (lambda x ((f x) f))) (lambda y (lambda g (g (* y y))))) 2) (lambda a a))

My question is in continuation to lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12) given the input: ...
1
vote
1answer
62 views

lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12)

given the input (((lambda f (lambda x (f x))) (lambda y (* y y))) 12) what does this step evaluate to: lambda x (f x) I am ...
5
votes
2answers
583 views

Does the underlying computational calculus in type theories affect decidability?

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers. I understand that modern type theory is inspired by Curry-Howard ...
3
votes
0answers
40 views

Is there an abstract architecture equivalent to Von Neumann's for Lambda expressions?

In other words, was a physical implementation modelling lambda calculus (so not built on top of a Von Neumann machine) ever devised? Even if just on paper? If there was, what was it? Did we make use ...
-2
votes
1answer
73 views

Lambda Expression Reduction

I am unable to solve the following lambda expression using both normal order (Call-by-name) and applicative order (Call-by-value) reduction. I keep getting different answers for both. This is the ...
0
votes
0answers
25 views

Lambda calculus self reducer with explicit redex selection

In "Efficient Self-Interpretation in Lambda Calculus", Mogensen presents a self-reducer in lambda calculus which leaves redex selection to the underlying reduction. Is there some example of a self-...
0
votes
1answer
45 views

Termination of Z combinator with call-by-value

I am trying to build my own λ-calculus interpreter. So far it supports both call-by-value and normal order. I now want to try recursion via fixed points. The $Y$ combinator works with normal order, ...
3
votes
0answers
25 views

Standardisation Theorem versus Leftmost reduction Theorem

According to Chris Hankin in his book (Lambda Calculus a Guide for Computer Scientists). A reduction sequence $\sigma: M_0 \to^{\Delta_0} M_1 \to^{\Delta_1}M_2 \to^{\Delta_2}\ldots $ is a standard ...
1
vote
0answers
18 views

Self reduction for fully introspective lambda calculus representations

For some representation scheme $\ulcorner \cdot \urcorner$, a self interpreter $R$ is a lambda expression where $R \ulcorner A \urcorner \underset{\beta}{=} A$, while a self reducer $E$ is a lambda ...
3
votes
0answers
72 views

Is it true that if $M : \forall \alpha . \left( \alpha \rightarrow \alpha \right)$ is a closed term then $M = \Lambda \alpha. \lambda x^{\alpha} . x$?

In system F, is every closed term $M$, which is of $\forall \alpha . \left( \alpha \rightarrow \alpha \right)$, $\alpha \beta \eta$-equivalent to $\Lambda \alpha. \lambda x^{\alpha} . x$? I have ...
2
votes
0answers
76 views

Normal Order Reduction - is Leftmost Outermost order simply Leftmost?

This is a quick question. I've been reading up on Lambda Calculus, and I see Normal Order as "outermost leftmost first", and Applicative Order described as as "innermost leftmost first". I think ...
0
votes
1answer
53 views

How to find a lambda term to complete a function?

I tried to complete this exercise but i stopped... Defining a $ \lambda $-term M such that: $$(<M,u>)<M,v> \: \simeq_{\beta} \: <M,u>$$ I chose $M=\lambda m \lambda a \lambda b \...

1
2 3 4 5
10