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.
225
questions
11
votes
3answers
716 views
Equivalent formulation of complexity theory in Lambda Calculus?
In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched.
...
11
votes
2answers
1k views
Why is lambda calculus a “calculus”?
The only definition of "calculus" I'm aware of is the study of limits, derivatives, integrals, etc. in analysis. In what sense is lambda calculus (or things like mu calculus) a "calculus"? How does it ...
11
votes
3answers
280 views
Calculus of Constructions: compress expression to its smallest form
I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient ...
11
votes
2answers
471 views
Does the System F with pairs have the strong normalisation and subject reduction properties?
It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
11
votes
2answers
369 views
Hereditary substitution with a universe hierarchy
I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types.
I'm wondering, are there any examples of hereditary substitution in ...
11
votes
1answer
1k views
What is the “question” that programming language theory is trying to answer?
I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
11
votes
2answers
546 views
What's the difference between reduction strategies and evaluation strategies?
From the evaluation strategy article on Wikipedia:
The notion of reduction strategy in lambda calculus is similar but distinct.
From the reduction strategy article on Wikipedia:
It is similar ...
11
votes
1answer
453 views
Extensionality of lambda calculus models
I'm translating a book on LISP and naturally it touches some elements of $\lambda$-calculus. So, a notion of extensionality is mentioned there alongside some models of $\lambda$-calculus, namely: $\...
11
votes
1answer
803 views
Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?
So I've been wondering if the Law of Excluded Middle (LEM) implies the so-called Axiom K in Martin-Löf's Intensional Type Theory. The Axiom K states that
$$\Pi_{A : Type} \Pi_{x : A} \Pi_{p : \text{Id}...
10
votes
3answers
538 views
Is there any known CCC closed under a probabilistic powerdomain operation?
Equivalently, is there a known denotational semantics for probabilistic higher-order functional programming languages? Specifically, is there a domain model of pure untyped $\lambda$-calculus extended ...
10
votes
1answer
657 views
Can affine lambda calculus solve every problem in P?
In Advanced Topics in Types and Programming Languages it is mentioned, in the chapter on sub-structural type systems, that a "carefully crafted" affine lambda calculus with a recursion combinator for ...
10
votes
1answer
294 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 ...
10
votes
1answer
728 views
How do you encode Lamping's abstract algorithm using interaction combinators?
Interaction combinators have been proposed as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to optimize interaction-net ...
10
votes
1answer
214 views
Program inversion algorithms for higher-order programs
The term program inversion
has multiple shades of meaning, but probably got started with
J. McCarthy's 1956 work The Inversion of Functions Defined by Turing Machines in the context of AI. By now ...
10
votes
1answer
1k views
Are optimal evaluators actually optimal?
The following term (using bruijn-indexes):
BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0)))))))))
...
10
votes
1answer
185 views
Reference for the undefinability of modulus of continuity functional in PCF?
Can someone point me to the reference for the non-definability of the modulus of continuity functional in PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$
Andrej Bauer has ...
10
votes
1answer
361 views
10
votes
0answers
336 views
Typed Lambda Calculus models and denotations
I'm trying to draw a general mental picture about the models and the
denotational semantics of the typed lambda calculus, in its different
variants.
I'm particularly interested in how the semantics ...
10
votes
0answers
285 views
A bijection between ordered lambda terms and rooted planar maps?
Consider the following recurrence in two parameters $n$ and $k$:
\begin{aligned}
NF(0,k) &= 0 \\
NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\
Neu(n,k) &= [n=1 \wedge k=1] + \sum_{l=1}^{n-1}\sum_{...
9
votes
3answers
1k views
How to make the Lambda Calculus strong normalizing without a type system?
Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
9
votes
3answers
365 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 ...
9
votes
2answers
324 views
What is the benefit of Krivine's notation?
I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
9
votes
2answers
451 views
Are a few hundred reduction steps too many to get the normal form of Y fac ⌜3⌝?
As I have been teaching the basis of λ-calculus lately, I have implemented a simple λ-calculus evaluator in Common Lisp. When I ask the normal form of Y fac 3 in ...
9
votes
1answer
463 views
Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?
On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the ...
9
votes
2answers
426 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 ...
9
votes
1answer
332 views
Reading list on rewriting systems?
I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
9
votes
1answer
505 views
What is the role of the Bicolored Calculus of Constructions?
So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
9
votes
1answer
254 views
Understanding the Proof of Strong Normalization of the Calculus of Constructions
I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong ...
9
votes
1answer
468 views
A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?
Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
8
votes
3answers
3k 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 ...
8
votes
2answers
723 views
Weakly normalizing + confluent = strongly normalizing?
I was reading this abstract and saw that they prove weak normalization and confluence. My limited understanding suggests that those two properties should provide strong normalization, which then ...
8
votes
1answer
250 views
Origin of Church encodings
In which paper did Alonzo Church first describe Church encoding? I can't find any articles that actually cite the paper, but I am interested in reading it.
8
votes
2answers
192 views
How to state the adequacy of an encoding of lambda calculus in itself?
In the paper Discriminating coded lambda terms - Henk Barendregt a coding $\ulcorner M \urcorner$ of a lambda term $M$ is a term such that $M$ (and its parts) can be reconstructed from it in a lambda-...
8
votes
1answer
407 views
PHOAS with extrinsic typing?
Parameterized Higher Order Abstract Syntax (PHOAS) is a representation of syntax trees that allows the host language's binding to be used to represent binding in the language being modelled, while ...
8
votes
1answer
408 views
Fixed points in dependent type theories
Most dependent type theories aim for some notion of correctness in two respects:
The type system must be decidable.
The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
8
votes
1answer
288 views
How to define eta-equivalence for F-omega types?
There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus:
via a plain relation $t_1 = t_2$,
via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
8
votes
0answers
45 views
Relationship between lambda-definability, specification and definability in model theory
I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts:
An element $a$ in the domain of a type $A_\sigma$ is ...
8
votes
0answers
271 views
Denotational semantics of System $F_\omega$ with recursive types and general recursion
Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion?
I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
8
votes
0answers
83 views
Decidability of equality between higher-kinded equirecursive types (or: between nonregular Böhm trees)
In §3 of Polytypic values possess polykinded types, Ralf Hinze described a calculus of types with higher-kinded recursive types. There is a fixed-point combinator $$\mu_\kappa : (\kappa \rightarrow \...
8
votes
0answers
409 views
Complete combinator basis for System F-omega
The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
8
votes
0answers
176 views
Equivalence of categories of directed complete posets
I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets.
Since I had no answer, I try here.
In the book ``Domains and Lambda-...
7
votes
4answers
755 views
Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?
I know very little about what I am talking about in what follows, so I appreciate any all help in pointing out all of my mistakes -- otherwise I won't be able to learn more and advance in my knowledge ...
7
votes
8answers
5k 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?
7
votes
3answers
783 views
What does it mean that there are differing views on how computations are represented on the Turing Machine?
For a given algorithm (eg reverse the items in this list) and a given type of Turing machine (eg the 3-state 2-symbol busy beaver reduced to 5-tuples) - is there a single simplest way that this ...
7
votes
2answers
830 views
Closed term and alpha-conversion
In the simply-typed lambda calculus, do we ever need alpha-conversion in a small-step call-by-value reduction of a term that is closed?
The evaluation rule that uses substitution is:
$(\lambda x.t_1)~...
7
votes
2answers
850 views
Translation from basic While-language to $\lambda$-calculus
Is there a simple way to translate programs written in a basic "While" language (such as Winskels Imp)?
I know about Church numerals and booleans, and I can see how if and while statements can be ...
7
votes
3answers
385 views
Are the $\lambda_I$-Calculus and the $\lambda_K$-Calculus equivalent?
I see here and there mention of the $\lambda_I$-Calculus (in which every variable must be used at least once) and the $\lambda_K$-Calculus (in which a variable can also be unused). Are they ...
7
votes
3answers
975 views
What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?
I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the ...
7
votes
3answers
345 views
When a type is a value?
In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
7
votes
2answers
264 views
Termination checking for Scott-encodings in System F with positive-recursive types
Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types.
All papers I have found use languages with constructors and case analysis (for example ...
