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.

248 questions
Filter by
Sorted by
Tagged with
57 views

Proof for a Lemma in Lambda Calculus

$\newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\length}[1]{\operatorname{len}\left(#1\right)}$ I am a starter in Lambda calculus, and I need to learn to prove lemmas and ...
187 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-...
192 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: ...
72 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 ...
1 vote
49 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 ...
72 views

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 .... 3 votes 0 answers 90 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}}{... 7 votes 0 answers 97 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 ... 2 votes 1 answer 153 views Intuitive way to handle variable binding Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ... 3 votes 0 answers 62 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 ... 2 votes 0 answers 58 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 ... 5 votes 1 answer 83 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: ... 0 votes 0 answers 142 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 ... 7 votes 0 answers 127 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{...
98 views

A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used ...
425 views

Is there an efficient beta-equivalence algorithm?

Is there an efficient algorithm to determine if two terms are beta-equivalent? Specifically, I am curious about simply-typed-lambda-calculus, so you can assume both terms are strongly normalizing. I ...
148 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 ...
446 views

Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete? I believe the answer is ...
1 vote
91 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?
509 views

Constructing terms of function types out of the empty type

If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we ...
174 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 ...
182 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 ...
121 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 ...
184 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 ...
195 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). ...
346 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, ...
99 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-...
100 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 ...
141 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 ...
388 views

Simple model of computation with homoiconicity

Is there a simple model of computation with homoiconicity? It would also be nice if, like beta reduction in lambda calculus, every step in execution yields a new valid program. Besides the lack of ...
516 views

Can factorial be encoded in the Kappa-calculus with fixed point operator?

Suppose we have a $\kappa$-calculus with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal ...
4k views

Implementation of alpha equivalence

I'm reading through "Type Theory & Functional Programming" by Simon Thompson and it says We shall not distinguish between expressions which are equivalent up to change of bound variable names ...
1 vote
39 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: ...
123 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 ...
247 views

Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?

Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices: ...
9k views

Realizability theory: difference in power between Lambda calculus and Turing Machines

I have three related subquestions, which are highlighted by bullet points below (no, they could not be split, if you are wondering). Andrej Bauer wrote, here, that some functions are realizable ...
115 views

Metrics for modelling convergence in the lambda-calculus

I wonder if there have been efforts to reconcile the measure approach to termination and Scott's domain theory or other topological models of computation. In other words, can we translate this measure ...
943 views

Can we derive Cubical Type Theory from Self-Types?

Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
1 vote
71 views

What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?

I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet. This is what I've thought about ...
79 views

Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs

Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union. For example, $S$ ...
7k views

What are the simplest turing-complete systems? [closed]

Lambda Calculus is very simple. Are there even simpler turing-complete systems? Which is the simplest of them all?
83 views

I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where $\alpha$ is any type (I subscript some terms with ...
169 views

Category theory lambda cube?

If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to? https://en.m.wikipedia.org/wiki/Lambda_cube
236 views

Categorical equivalent of higher order logic

From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
107 views

Beta reduction and vacuous lambda abstraction [closed]

Suppose we have the following typed lambda term (where $s$ does not occur in E (which is of type $s \to p$) and $s$ and $s'$ have the same type), and want to apply $\beta$-reduction: \$(\lambda s. E)\, ...
123 views

Would it be possible to derive transp natively from Path, Interval and typecase?

Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm ...
349 views

Busy Beaver Equivalent for the Untyped Lambda Calculus

In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus: Over all terms in the ULC composed of ...
1 vote
52 views

A substitution to add variables in the context

I'm doing type-inference in a dependently typed language, using (as is commonly done) a λ-calculus with explicit substitutions like that of Abadi (with a representation based on debruijn indices) in ...