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

learn more… | top users | synonyms

5
votes
0answers
167 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 ...
3
votes
1answer
54 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 ...
5
votes
0answers
68 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 ...
4
votes
1answer
69 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 ...
7
votes
1answer
203 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 ...
9
votes
1answer
279 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 ...
12
votes
3answers
427 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 ...
10
votes
2answers
124 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 ...
9
votes
0answers
58 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 ...
10
votes
1answer
857 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))))))))) ...
5
votes
1answer
44 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 ...
4
votes
0answers
44 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, ...
5
votes
0answers
68 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
votes
0answers
30 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 ...
4
votes
1answer
68 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 ...
1
vote
0answers
56 views

Optimal reduction using token-passing nets

I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis ...
7
votes
2answers
179 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 ...
8
votes
1answer
202 views

Is `sort` typeable on elementary affine logic?

The following λ-term, here in normal form: ...
7
votes
1answer
223 views

An example where smallest normal lambda term is not fastest

Let the $size$ of $\lambda$-terms be defined as follows: $size(x) = 1$, $size(λx.t) = size(t) + 1$, $size(t s) = size(t) + size(s) + 1$. Let the complexity of a $\lambda$-term $t$ be defined as ...
4
votes
1answer
57 views

What is the formal definitions of the reduction related to the “call/cc” (call with the current continuation) operator?

In lambda calculus or in combinatory logic we formally define reduction/expansion rules for terms (and in their typed variants reductions must preserve the type). Then we can talk about properties of ...
-1
votes
1answer
183 views

What is the simplest known solver for a np-complete problem?

Lets define the simpler of two terms as the one with shortest description length on the untyped λ-calculus. Trying to find the simplest solver for a np-complete problem, I've got this: ...
10
votes
1answer
164 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 ...
2
votes
1answer
151 views

Would a proof that the traveling salesman algorithm can't be encoded on LAL also prove P!=NP?

An answer to the traveling salesman (and similar) problems can be easily verified on light lambda-calculi. Also, if I understand correctly, the light lambda-calculi can compute every polinomial-time ...
6
votes
0answers
85 views

Is it possible to unambiguously read back λ terms from interaction nets without node types?

A class of lambda terms can be evaluated using Lamping's abstract algorithm - that is, converting them to interaction nets and applying a set of rules. In order to get the result, you have to read ...
4
votes
1answer
46 views

Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't ...
13
votes
2answers
421 views

Smallest possible universal combinator

I am looking for the smallest possible universal combinator, measured by the number of abstractions and applications required to specify such a combinator in the lambda calculus. Examples of universal ...
2
votes
1answer
81 views

Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

Let f and g be lambda terms in the normal form, such that f is intensionally different from ...
5
votes
2answers
118 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 ...
0
votes
1answer
54 views

Why is the polymorphic weight 1

I am reading through through a paper called HMF: Simple Type Inference for First-Class Polymorphism by Daan Leijen of Microsoft Research. In the paper it describes how to calculate the polymorphic ...
4
votes
0answers
49 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 ...
9
votes
2answers
429 views

Is there a typed lambda calculus which is consistent and Turing complete?

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...
3
votes
1answer
61 views

What is contextual equivalence ignoring non-termination called?

Contextual equivalence ($M_1 \cong_{ctx} M_2$) is often defined as: $C[M_1] \Downarrow V \iff C[M_2] \Downarrow V$ Which is to say for any context $C$, $C[M_1]$ terminates with value $V$ iff ...
13
votes
3answers
480 views

Why do constructivists not seem to care too much about call/cc

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
8
votes
1answer
315 views

Why it's impossible to declare an induction principle for Church numerals

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
2
votes
0answers
69 views

Resources for Church's paper “An Unsolvable Problem of Elementary Number Theory”?

I'm trying to understand and breakdown into simple English Church's paper for "An Unsolvable Problem of Elementary Number Theory" but I'm not finding anything useful online, only citations and links ...
6
votes
2answers
396 views

How would a theory of computation course that culminated in lambda-calculus as “the” model of computation, instead of Turing machines, look like?

Currently, our ToC (Theory of Computation) courses are designed with the following progression of topics: Finite automata and regular languages Pushdown automata and context-free languages Turing ...
1
vote
3answers
387 views

Why is lambda calculus so “function” oriented?

I've always had this question nagging at me subconsciously but have never been able to intuitively grasp it. Why does $\lambda$-calculus have a functional notation? Why is everything a function? It ...
5
votes
3answers
281 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 ...
21
votes
2answers
2k views

What was the original intent for the creation of Lambda calculus?

I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church ...
4
votes
1answer
85 views

In which posets is the set of compact elements downwards closed?

In a poset $(D, \sqsubseteq)$, a compact element is an element $d \in D$ such that for every directed set $A$ which happens to have a supremum $\bigsqcup A \in D$ with $d \sqsubseteq \bigsqcup A$, it ...
9
votes
2answers
608 views

How exactly does lambda calculus capture the intuitive notion of computability?

I've been trying to wrap my head around the what, why and how of $\lambda$-calculus but I'm unable to come to grips with "why does it work"? "Intuitively" I get the computability model of Turing ...
-2
votes
1answer
42 views

How is does a scheme lambda function relate to lambda calculus?

For example: (define fact (lambda (n) (if (< n 2) 1 (* n (fact (- n 1))))) How is this an example of applied lambda calculus? I tried to read the ...
10
votes
3answers
362 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 ...
15
votes
3answers
392 views

Can typed lambda calculi express *all* algorithms below a given complexity?

I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming ...
3
votes
1answer
125 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 ...
5
votes
1answer
100 views

Commutativity of addition in polymorphic lambda calculus

In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding: $polyint = \forall t . (t \to t) \to t \to t$ Addition ...
7
votes
1answer
174 views

Church-Rosser equivalent for concatenative languages?

Looking at the striking parallels between combinatory logic and concatenative languages makes me wonder how many theorems of the former hold in the latter. The Church-Rosser theorem is particularly ...
0
votes
0answers
119 views

Is there an algorithm to find whether 2 combinators form a Turing-complete system?

It is known that K = (λx.(λy.x)) and S = (λx.(λy.(λz.((x z) (y z))))) define a turing complete system, and we know procedures to ...
15
votes
2answers
558 views

Fixed points in computability and logic

This question has also been posted on Math.SE, http://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic I hope it is ok to also post it here. If not, or if it is too ...
4
votes
1answer
161 views

What is a term of the type $\bot\rightarrow A$?

The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial: \begin{align} \bot&\vdash\bot \\ \hline \bot&\vdash A \\ \hline ...