Tagged Questions

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

6
votes
1answer
67 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
93 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
382 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
108 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
106 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
238 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
268 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
412 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 ...
5
votes
1answer
93 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 ...
4
votes
1answer
410 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
128 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 ...
16
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
61 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
66 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
134 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
218 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] + ...
5
votes
0answers
142 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 ...
57
votes
6answers
21k 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
137 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
75 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\; ...
15
votes
1answer
151 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
90 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
312 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
72 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 ...
1
vote
2answers
414 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
270 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
53 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
155 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
203 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
219 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
122 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 ...
-2
votes
8answers
527 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
198 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?
8
votes
1answer
277 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 ...
16
votes
1answer
455 views

What is the difference between arrows and exponential objects in a cartesian closed category?

In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
13
votes
3answers
533 views

funsplit and polarity of Pi-types

In a recent thread on the Agda mailing list, the question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. My understanding is that $\eta$ laws come with negative ...
8
votes
1answer
159 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$ ...
7
votes
3answers
189 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 ...
11
votes
1answer
540 views

Can Scheme's call/cc implement all known control flow structures?

The page "Advanced Scheme: Some Naughty Bits" states: Continuations are a powerful control-flow construct from which nearly any other control-flow structure [...] may be derived. I thought ...
9
votes
1answer
193 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 ...
16
votes
2answers
302 views

Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?

I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).: If A ...
5
votes
1answer
195 views

Characterizing closure under expansion/reduction for big-step semantics?

Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics. In a big step semantics, you give a relation $e ...
8
votes
0answers
463 views

What's the expressive power of Simply Typed Lambda calculus?

The standard approach to simply typed lambda calculus considers computations over Church numerals. If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) ...
3
votes
1answer
180 views

Exponential blowup in Simple Proof of a theorem of Statman by Mairson

I'm studying "A simple proof of a theorem of Statman" by H.G. Mairson. At page 4, he encodes set/type theory in lambda calculus. In particular, note che "op" trick in the definition of $eq_{k+1}$. ...
10
votes
1answer
262 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: ...
7
votes
1answer
266 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 ...
5
votes
2answers
496 views

Do Higher-Order Functions provide more power to Functional Programming?

My original question was: Is Kappa calculus less powerful than Lambda calculus? Does the lack of Higher-Order functions on a programming language excludes some programs that could only be written in ...
7
votes
1answer
199 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.
3
votes
2answers
164 views

Labels for terms in the lambda calculus

In the lambda calculus, are there commonly accepted names for $x$ and $M$ when they appear in $\lambda x [M]$ ? Something along the lines of "binder" and "bindee"?
8
votes
0answers
497 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...