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

0
votes
0answers
14 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 ...
1
vote
1answer
14 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 ...
8
votes
2answers
239 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 ...
6
votes
1answer
157 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
47 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 ...
5
votes
1answer
266 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
335 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
129 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 ...
19
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
66 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 ...
8
votes
2answers
533 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
24 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
323 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 ...
14
votes
3answers
287 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
86 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
78 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
121 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
105 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 ...
12
votes
2answers
457 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
138 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 ...
6
votes
1answer
149 views

Are there presentations of set theory in terms of lambda-calculus?

I am planning to implement in software a set theory language, based on a binary function, which in set theory is the so called adjunction operation: $f(x, y) = x \cup$ {y}. Therefore, a presentation ...
13
votes
1answer
304 views

Scott's stochastic lambda calculi

Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
10
votes
1answer
316 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 ...
5
votes
1answer
425 views

Is this behavior in a programming language inconsistent?

I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem: The identity function ...
6
votes
1answer
105 views

A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
5
votes
1answer
559 views

Historic Relationship between Typed Lambda Calculus and Lisp?

I was having a discussion with a friend recently (who is an advocate of strongly typed languages). He made the comment: The inventors of Lambda Calculus always intended it to be typed. Now we ...
7
votes
1answer
135 views

Are there stronger notions of equivalence over lambda terms than beta equivalence?

I should add the context that I am concerned with strongly normalizing systems like System-F. I have what I consider a very strong notion of equivalence for lambda terms that goes something like the ...
18
votes
3answers
2k views

P and NP classes explanation through lambda-calculus

In the introduction and explanation P and NP complexity classes often given through Turing machine. One of the model of computation is the lambda-calculus. I understand, that all of models of ...
4
votes
1answer
67 views

Upper bound on Chaitin's constant for lambda calculus and SKI combinatory logic

I'd like to have proof that Chaitin's constant for lambda calculus and/or SKI combinatory logic is pretty small. I've found some approximations (accurate to about 63 binary digits) for truing machines ...
2
votes
0answers
73 views

How to translate general recursion into a set of $\mu$-recursive operator applications?

I'm trying to find a scheme to translate a functional language with let rec into a set of primitives called "generalized arrows", i.e. $\kappa$-calculus with ...
5
votes
1answer
147 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 ...
10
votes
0answers
232 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] + ...
6
votes
0answers
168 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 ...
64
votes
7answers
22k views

What is the contribution of lambda calculus to the field of theory of computation?

I'm just reading up on lambda calculus to "get to know it". I see it as an alternate form of computation as opposed to the Turing Machine. It's an interesting way of doing things with ...
6
votes
0answers
143 views

Equivalence of categories of directed complete posets

I asked this question there: http://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 ...
4
votes
0answers
91 views

Defining a calculation-reversing function in the lambda calculus

Obviously, lambda calculus functions are not in general invertible. That is, there is no lambda function $V$ (for inVerse) such that $$ (V\; A)\; (A\; B) \to B $$ for every $A$ and $B$ such that $(A\; ...
16
votes
1answer
184 views

A Lambda calculus for invertible (r-Turing computable) functions

I'm interested in the concept of "r-Turing completeness", as defined by Axelsen and Glück (2011). A system is r-Turing complete if it can compute the same set of functions as a reversible Turing ...
-3
votes
1answer
99 views

Are two unbound variables alpha-equivalent? [closed]

Let's say we have the following cases: $a =_\alpha b$ $a =_\alpha a$ Which of the above cases are $\alpha$-equivalent? Or does $\alpha$-equivalence has no meaning in the context of just variables? ...
4
votes
3answers
401 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?
2
votes
0answers
79 views

Evaluation contexts: outside-in vs inside-out

I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
2
votes
2answers
605 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
2answers
301 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 ...
1
vote
0answers
60 views

Is combinatory strong reduction equivalent to lambda beta-eta reduction?

I'm familiar with the correspondence between combinatory logic and $\lambda$-calculus at equality level, ie $=_{\beta\eta}$ corresponds to $=_s$ (the equivalence relation generated by strong ...
5
votes
0answers
171 views

Regular languages in lambda calculus

With Turing machines, by imposing certain restrictions on the form of the transition function, one can get a machine that accepts only regular languages. I am wondering what is the counterpart in ...
2
votes
2answers
224 views

Is there a space efficient way to represent numbers on the lambda calculus?

This is something I've been thinking. While it is agreed that Lambda Calculus is equivalent to a Turing Machine in power, is it actually so? Church Numerals are not very space efficient and I'm not ...
1
vote
3answers
224 views

“lambda” term usage in programming

could any one please let me know what is the relation between "lambda" and anonymous functions in programming? in other words why we say lambda function to an anonymous function? I am here trying to ...
1
vote
1answer
130 views

A few questions about ISWIM

I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
-1
votes
8answers
706 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?
4
votes
2answers
204 views

Is there a systematic method for constructing lambda calculus terms that can distinguish between inputs?

For example, finding terms $\vec{a}$ such that: $\vec{a}(\lambda x.x) = T\\\vec{a}(\lambda xy.x) = F$ Is there a systematic method for finding terms with these types of constraint?
9
votes
1answer
372 views

η-conversion vs extensionality in extensions of lambda-calculus

I'm often confused by the relation between η-conversion and extensionality. Edit: According to comments, it seems I'm also confused about the relation between extensional equivalence and ...