# 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.

249 questions
Filter by
Sorted by
Tagged with
97 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$. ...
• 121
60 views

### Proof for a Lemma in Lambda Calculus

$\newcommand{\freevars}{\operatorname{FV}\left(#1\right)}$ $\newcommand{\length}{\operatorname{len}\left(#1\right)}$ I am a starter in Lambda calculus, and I need to learn to prove lemmas and ...
• 101
202 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: ...
• 23
73 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 ...
• 133
1 vote
51 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 ...
• 133
77 views

• 521
1 vote
92 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?
177 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 ...
• 433
192 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 ...
• 143
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 ."  is a reference to a 300-page book with no further details and ...
• 61
188 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 ...
• 1,910
198 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). ...
• 29
356 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, ...
101 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 ...
146 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 ...
• 175
1 vote
41 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: ...
• 2,724
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 ...
150 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 ...
• 521
955 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&...
• 3,045
1 vote
72 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 ...
• 119
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$ ...
• 105
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 ...
• 105
172 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
• 163
242 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.
• 767
436 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 ...