Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [lambda-calculus]

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

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

Böhm tree with pairs (product types)

I am looking for references for a notion of Böhm tree for the λ-calculus with pairs and projections (and the reduction rule $\pi_i\, \langle t_1, t_2\rangle \longrightarrow t_i$). I'm only aware of ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
3 votes
1 answer
130 views

Is there a full abstraction result for an untyped lambda calculus?

Famously, the denotational semantics of PCF in Scott domains is not fully abstract. But by adding the parallel or construct to PCF, a fully abstract semantics can be obtained. Is there an analogous ...
Nick Rioux's user avatar
1 vote
1 answer
62 views

Are there any books or articles that contain information on the P weak omega or second order predicate calculi?

I have been trying to learn about the lambda cube, but cannot find any sources covering the P weak omega and P2 nodes. Is the problem that these nodes are not frequently used/ offer little benefits ...
hugofin's user avatar
  • 11
10 votes
2 answers
360 views

What are pertinent references to cite on Scott domains?

Scott domains are often presented as having been introduced in 1969. However, the first (but numerous!) papers are from the 1970s, so it is not easy to know what the pertinent references are. My two ...
sparusaurata's user avatar
7 votes
3 answers
647 views

Example of a term in system F which is not typable in the simply typed lambda calculus

What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus? More precisely, I am looking for a ...
Gro-Tsen's user avatar
  • 841
2 votes
1 answer
117 views

Is beta normalization used for program optimization?

Beta normalization reduces a lambda term to its beta normal form, if it exists. The beta normal form is a computationally equivalent term with no "redundant" computation, in a sense; for ...
Hirrolot's user avatar
  • 105
4 votes
1 answer
184 views

Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

What is the precise connection between: strong normalization of the simply typed $\lambda$-calculus, and cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent ...
Gro-Tsen's user avatar
  • 841
2 votes
0 answers
90 views

Variable opening in locally-nameless representation

Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
phdstudent's user avatar
0 votes
0 answers
88 views

Can lambda-calculus, or other formal systems / calculi, be represented using set theory?

Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad. If I have ...
The Pointer's user avatar
-1 votes
1 answer
84 views

What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

I was given an exercise that asked me to assign a simple type to the lambda term: $$ \lambda a.a(\lambda yt.t)(ya) $$ but I couldn't find one, furthermore, the lambda term seems untypable to me ...
Domiziano Scarcelli's user avatar
-1 votes
1 answer
170 views

Locally nameless representation implementation

ORIGINAL: I am programming a functional compiler and found out about locally nameless representation (using de brujin indeces for bound variables and names for free variables). I just don't understand ...
Deonisos's user avatar
-1 votes
1 answer
115 views

Is it necessary to apply alpha conversion in this term to perform beta reduction in lambda calculus?

I am trying to prove that the expression ((λx.(λx.x))(ab)) does not require alpha conversion for beta reduction since there is no variable overlap, but how could I demonstrate this more formally?
AdrianGarciaB's user avatar
4 votes
0 answers
316 views

How to prove that a language that allows infinite loops is still not Turing-complete?

CPS translations will always use pairs, either explictly or by currying. Though I can't find a reference for that, I'm assuming this is a necessary condition (I'd appreciate a reference if someone has ...
paulotorrens's user avatar
1 vote
1 answer
94 views

Intuition behind UTT's internal logic

The "internal logic" of type theory UTT is defined in LF as follows: What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
user175254's user avatar
2 votes
1 answer
578 views

Is classical lambda calculus grammar an `LL(k)` one?

I am playing with a lambda calculus and faced a question I find hard to reason about. On the screenshot you may find the lambda calculus grammar. Is it an instance of the ...
Zazaeil's user avatar
  • 212
1 vote
0 answers
78 views

Is it possible to define beta reduction for PHOAS?

I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml: ...
Hirrolot's user avatar
  • 105
5 votes
2 answers
351 views

Lambda-calculus: Beta-equivalent terms have the same type

In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type? My guess is that I should use the subject reduction, and maybe the ...
Bob's user avatar
  • 381
0 votes
0 answers
147 views

On the use of Turing machines for computational complexity

Almost always in the study of computational complexity, the Turing machine is used as a model. On the other hand, the untyped lambda calculus is in a sense "simpler" than any Turing machine: ...
Wasabi Kurosawa's user avatar
0 votes
0 answers
92 views

Simple Lambda Calculus Question

For any 2 strongly normalizing terms in the simply typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong ...
Abhishek Manikandan's user avatar
7 votes
1 answer
413 views

The precise definition of Normalization By Evaluation?

The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language: The ...
Hirrolot's user avatar
  • 105
5 votes
2 answers
272 views

Complexity of convertibility in simply typed λ-calculus with sums

For the simply typed λ-calculus with only the function type →, the complexity of deciding βη-equivalence is well-understood: it's TOWER-complete (as mentioned here). I expect the same should be true ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
1 vote
0 answers
69 views

Interpretation of the degree of a redex

In Girard Proofs and Types, The degree of a type is defined as follows $$\begin{align*}\partial(T_i)&=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\...
Sam Ezeh's user avatar
0 votes
1 answer
207 views

Fixed-point combinator on arithmetic functions

The question is about this Racket program: ...
Cyker's user avatar
  • 779
2 votes
0 answers
149 views

How to implement the next type inference algorithm?

Here I mean only simple typed Lambda calculus / Combinatory logic. Notation: Combinatory logic terms: $F, X_i, Y_i$. Term application: $(F*X_1)$. Type variables $x_i,y_i$. Type assignment: $X:x_i$. ...
Oleg Dats's user avatar
  • 121
2 votes
2 answers
443 views

What is the computational power of the Calculus of Constructions?

The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: ...
Jonathan's user avatar
2 votes
1 answer
79 views

Question about "Free-ness" of Free SCWF

In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF. My ...
EDJ's user avatar
  • 133
1 vote
1 answer
72 views

Question in relating STLC and Free CCC

In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph) My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
EDJ's user avatar
  • 133
4 votes
1 answer
161 views

Is there a standard way to "point" at subterms in a lambda expression?

Let's say I have a lambda expression $$ (\lambda x . (\lambda w.ww)x) y $$ There are a bunch of subterms: $(\lambda x . (\lambda w.ww)x) y$ $\lambda x . (\lambda w.ww)x$ $(\lambda w.ww)x$ $\lambda w ....
azani's user avatar
  • 143
8 votes
1 answer
350 views

What are the application of Scott-Topology in theoretical computer science?

During a work I came across the Scott-Topology and I see that Scott-continuous functions show up in the study of models for lambda calculi. What I cannot understand is how this enrich the lambda-...
micrus's user avatar
  • 91
3 votes
0 answers
109 views

Call-by-value solvability

Background There are two fairly common definitions of solvability. The general one states that the term can be used to get any chosen result (i.e. normal form):$$T\text{ solvable} \overset{\text{def}}{...
xavierm02's user avatar
  • 556
9 votes
1 answer
169 views

What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the ...
paulotorrens's user avatar
2 votes
1 answer
188 views

Intuitive way to handle variable binding

Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ...
A confused dove's user avatar
3 votes
0 answers
84 views

Expressive power of lambda-calculus with restricted application

Consider a syntactic restriction of the (untyped) $\lambda$-calculus in which an application cannot have another application as an immediate subterm. More precisely, restricted terms ($R,S,...$) and ...
pbaren's user avatar
  • 653
2 votes
0 answers
66 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 ...
Maman's user avatar
  • 121
5 votes
1 answer
90 views

Can a normal form term be extensionally equivalent to a term with no WHNF?

For convenience I'm using using the combinators SKIBCMTV I notice that it's possible to have a normal-form term extensionally equivalent to a term which has no normal form: ...
dspyz's user avatar
  • 916
0 votes
0 answers
168 views

What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?

There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...
MaiaVictor's user avatar
  • 3,137
7 votes
0 answers
140 views

Are the non-lazy / non-weak semantics of the $\lambda$-calculus related to weak evaluation?

Vague question The most common semantics of the call-by-name $\lambda$-calculus (Hyland/Wadsworth’s observational equivalence $\approx_\text{HNF}$ and Morris’s observational equivalence $\approx_\text{...
xavierm02's user avatar
  • 556
1 vote
0 answers
102 views

Is there some n such that lambda calculus with only n variables is Turing-complete?

Typically in lambda calculus you have an infinite stock of variables. Could we get away with a finite set?
Benjamin Grange's user avatar
8 votes
0 answers
193 views

$\lambda$-definability and structure preserved by homomorphisms

I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it. Some prelimary definitions. A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
Andrew Bacon's user avatar
3 votes
1 answer
353 views

Fixed points of fixed-point combinator?

A fixed point f of a fixed-point combinator would be a function that has itself as a fixed point: f(f) = f. The only such ...
GeoffChurch's user avatar
5 votes
1 answer
156 views

$\eta$-reduction not locally confluent on well-typed terms

This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]." [20] is a reference to a 300-page book with no further details and ...
capor's user avatar
  • 61
10 votes
0 answers
223 views

What is the "standard" lambda-calculus model for bicartesian closed categories?

(I'm familiar with the lambda-calculus, less so with its categorical models.) It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
gasche's user avatar
  • 2,040
5 votes
1 answer
270 views

Alternatives to Normalization by Evaluation

Reading about lambda calculus I got the impression that normalization is evaluation. So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel). ...
nbe's user avatar
  • 59
3 votes
2 answers
587 views

Are there strongly normalizing lambda terms that cannot be given a System F type?

I know that all well-typed System F terms are strongly normalizing, but is the converse true as well? In other words, does System F typeability precisely characterize program termination? (And if so, ...
Lionel Parreaux's user avatar
2 votes
1 answer
109 views

Typing inference as a map on abstract syntax trees

Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-...
user avatar
3 votes
0 answers
106 views

CCCs, computational calculi and point-surjectivity

The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $U$ that has some relationship to its exponential object $U^U$ e.g. a retraction ...
alessio-b-zak's user avatar
4 votes
1 answer
169 views

Structural normalization algorithm for the simply typed lambda calculus

I would like to know if there is a (piecewise) structural normalization algorithm for the simply typed lambda calculus. By structural I mean a recursive function that only calls itself on subterms of ...
Couchy's user avatar
  • 195
2 votes
1 answer
91 views

Nominal Tree Languages i.e. with Binders and Infinite Symbols?

I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence. I've found so far: ...
Joey Eremondi's user avatar
2 votes
1 answer
148 views

Phonology and lambda calculus

I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
Jacob Hjortmann's user avatar
5 votes
0 answers
178 views

Applications of solvability in the λ-calculus

What are applications of solvability / unsolvability, and of operational characterizations of solvability? Solvability In the (untyped pure call-by-name) $\lambda$-calculus, a closed term is said to ...
xavierm02's user avatar
  • 556

1
2 3 4 5 6