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.
265
questions
6
votes
1
answer
113
views
Can you assign a type to any term of the λEA-calculus?
The untyped language of System-F and similar is the λ-calculus. That language has terms that can't be typed on System-F, λx.(x x) λx.(x x) being the most obvious ...
- 3,117
12
votes
1
answer
349
views
Eta expansion in the pattern lambda calculus
Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.
http://www.sciencedirect.com/science/article/pii/S0304397508000571
In some sense, a pattern is a tree of variables ...
8
votes
1
answer
303
views
Resources (books, etc) to learn about concurrency theory
I want to know more about concurrency theory from a formal/mathematical point of view, I know there are a lot of computer science branches that relates to concurrency theory like process algebra, ...
3
votes
1
answer
172
views
Krivine's notation for lambda-terms [duplicate]
Krivine in his book (Lambda-calculus: Types and Models) introduces the grammar of lambda-terms and then abbreviations to denote them. The grammar itself is not ambiguous: Lambda-terms are
obtained by ...
- 103
2
votes
1
answer
715
views
Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive?
I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is:
Consistent/...
- 3,117
4
votes
0
answers
65
views
Finite intersection property of polymorphic type families
Let $\Phi$ be a type functor definable in polymorphic lambda calculus:
$$ \alpha : * \vdash \Phi(\alpha) : * $$
$$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$
Suppose further ...
- 611
8
votes
0
answers
179
views
deciding $\beta$-equality of planar lambda terms
Mairson showed that the problem of computing the $\beta$-normal form of a linear lambda term (or equivalently, computing its principal type) is complete for polynomial time.
Harry Mairson. Linear ...
- 4,431
4
votes
1
answer
285
views
What, in simple terms, are the restrictions imposed by Elementary Affine Logic?
The answer to my last question on the subject made several insightful points on how EAL could be used as the basis of a practical programming language, which, in turn, could be evaluated using the ...
- 3,117
5
votes
1
answer
123
views
Inference in typed lambda calculus theories
I'd like to do automated inference, say solving word problems or reducing to normal form, in an equational theory of the typed lambda calculus (with product and unit types). Equivalently, in category-...
6
votes
1
answer
291
views
Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?
If we extend the Calculus of Constructions with Fix, we gain a lot of expressivity for barely no added complexity. That includes being able to derive induction, perform large eliminations, prove ...
- 3,117
14
votes
0
answers
419
views
Are there simple core languages which are consistent and expressive?
The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
- 3,117
1
vote
2
answers
233
views
Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?
What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?
- 37
1
vote
2
answers
3k
views
Is iszero of the untyped lambda calculus sound and complete? [closed]
I am using the following definitions in the notation of Haskell. In case it matters, I would like to use only the $\alpha,\beta,\eta$ reductions rather than the Haskell evaluation rules.
...
- 173
2
votes
0
answers
113
views
Can a fixed point combinator find the fixed point of a function that has no fixed point? [closed]
A fixed point combinator is supposed to find the fixed point of any function. Yet I am wondering what if a function happens to have no fixed point, such as the add1 ...
- 173
3
votes
2
answers
189
views
Why is the multi-step reduction of semantics reflexive?
I was reading Programming Languages and Lambda Calculi, which defines the multi-step reduction to be the reflexive-transitive closure of the one-step reduction. (Page 15, $\twoheadrightarrow_r$ is the ...
- 173
11
votes
1
answer
900
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}...
- 777
7
votes
1
answer
348
views
Do we care about confluence because of unique normal forms?
Confluence implies uniqueness of normal forms, which is great. It is also much simpler to reason about, allowing more reusable proofs (indeed I don't imagine a way to prove UN directly for the $\...
- 181
2
votes
1
answer
370
views
Can recursion be replaced with a finite set of higher-order functions? [closed]
I am wondering if there is some proof that all recursive algorithms can be rewritten to use some known set of higher-order functions instead of recursion. I'm talking about functions like fold, map, ...
15
votes
2
answers
483
views
(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?
From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to ...
- 5,255
17
votes
1
answer
1k
views
How can non-terminating $\lambda$-terms be turned into fixed-point combinators?
I've been thinking about these questions:
Is there a typed lambda calculus which is consistent and Turing complete?
https://cs.stackexchange.com/questions/65003/if-%CE%BB-x-x-x-has-a-type-then-is-...
- 13.7k
2
votes
0
answers
178
views
Connection between nonmonotonic logic and type theory (lambda calculus)
There is known connection between classical and modal logics and type theory (lambda calculus), but are there connections between nonmonotonic logics (e.g. defeasible logic) and type theory (lambda ...
- 409
-3
votes
2
answers
3k
views
How to interpret Church numbers and the successor function in Lambda calculus [closed]
Consider the first two Church numbers:
$\mathbf{0}=\lambda a.\lambda b.b$
$\mathbf{1}=\lambda a.\lambda b.(a)b$
and the successor function:
$\mathbf{Suc}=\lambda a.\lambda b.\lambda c.(b)((a) b)c$....
- 95
3
votes
1
answer
629
views
Does the simply typed lambda calculus have general iteration?
In more expressive calculi such as System F, the Church numerals, by virtue of their design, allow for iteration over an arbitrary type. Can this effect be replicated in the simply typed case?
To be ...
- 247
5
votes
0
answers
104
views
Characterisation of the BCIW definable functions
Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.)
I ...
- 443
10
votes
0
answers
420
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 ...
- 668
4
votes
1
answer
405
views
Enumerating all simply typed lambda terms of a given type
How can I enumerate all simply typed lambda terms which have a specified type?
More precisely, suppose we have the simply typed lambda calculus augmented with numerals and iteration, as described in ...
- 652
4
votes
1
answer
188
views
Translating typed functional language to untyped lambda calculus
Defining a typed function in haskell,
double::Integer->Integer
double a = a + a
And we can get an untyped version of double and let's call it double' to ...
- 41
12
votes
1
answer
484
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 ...
- 259
7
votes
4
answers
1k
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 ...
- 503
-1
votes
1
answer
676
views
Understanding between lambda-calculus and other abstract machines (like Turing machine and Markov algorithm)
If we look on abstract machines we could noticed analogue with modern computers (of course). What I mean? I mean this points:
1. Model of implementer (In Turing machine it is description of head, ...
- 25
3
votes
1
answer
562
views
Can all mathematical operations be encoded with a Turing Complete language? [closed]
In High School Computing I was taught the Structured Program Theorem - that you could implement any mathematical operation using:
Sequence
Selection
Iteration
After completing a Computer Science ...
- 2,581
17
votes
2
answers
2k
views
How is Lambda Calculus a specific type of Term Writing system?
Church was associated with the Simply Typed Lambda Calculus. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus.
When John ...
- 2,581
8
votes
0
answers
362
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]...
- 161
25
votes
2
answers
4k
views
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
- 353
2
votes
1
answer
246
views
Algorithm for extensional equality in combinator calculus
I'm dealing with combinator calculus, using the $S$ and $K$ combinators as a basis. Sometimes my code generates expressions that define equivalent functions, such as
$$
(S\, K\, K) \qquad\text{and}\...
- 699
4
votes
0
answers
341
views
Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking
I need an extension of System $F_\omega$ with subtyping, and where the variance of type constructors is reflected in their kind. Unfortunately, System $F^\omega_{<:}$, as defined in chapter 31 of ...
- 501
2
votes
1
answer
132
views
Composition in explicit substitutions
In the classical λσ calculus of explicit substitutions, there is the following rewrite rule:
(a[s])[t] ==> a[s ∘ t]
where ...
- 390
4
votes
0
answers
267
views
Is it possible to implement tail recursion inside a lambda calculus built on top of functions?
Inside a lambda calculus implementation for ECMASCript 6, we are trying to implement new constructs such as type tags for strong typing, and conditionals such as the ...
- 141
5
votes
2
answers
430
views
Is there a "lambda cube" for interaction nets?
The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about ...
- 3,117
6
votes
1
answer
356
views
What type system fits the subclass of λ-terms that can be reduced optimally?
There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
- 3,117
9
votes
1
answer
543
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 ...
- 777
13
votes
3
answers
843
views
What are the negative consequences of extending CIC with axioms?
Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
- 777
14
votes
2
answers
477
views
Church-Rosser property for dependently typed lambda calculus?
It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations ...
- 777
14
votes
0
answers
257
views
historical question: earliest description of beta-normal terms together with "neutral" terms in lambda calculus?
A bit of "folklore" in lambda calculus is the idea of characterizing the class of $\beta$-normal terms inductively as a syntactic category ($R$) defined in mutual induction with an auxiliary syntactic ...
- 4,431
11
votes
1
answer
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)))))))))
...
- 3,117
5
votes
1
answer
101
views
Is it possible to evaluate interaction combinators efficiently using a path-traveling strategy?
Interaction combinators can be evaluated using a path traversing strategy. That is, instead of applying annihilation/commutation rules to active pairs, one simply walks through the graph using a 2-...
- 3,117
4
votes
0
answers
67
views
Is the question about closed reduction using token-passing nets still open?
The question about possible implementation of closed reduction using token-passing nets is asked on page 17 in Token-passing Nets for Functional Languages by Jose Bacelar Almeida, Jorge Sousa Pinto, ...
6
votes
0
answers
148
views
Is higher-order unification decidable for terms without abstractions within applications?
Consider the problem of higher order unification - that is, finding a substitution for the equation a = b, where a and ...
- 3,117
8
votes
2
answers
245
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-...
- 181
5
votes
1
answer
259
views
How can you encode natural numbers operations on interaction combinators?
The church-encoding for natural numbers is a natural mean of implementing addition, multiplication and so on on the lambda calculus. Interaction nets are said to be an alternative universal ...
- 3,117