The tag has no wiki summary.

learn more… | top users | synonyms

4
votes
0answers
91 views
+50

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 ...
54
votes
6answers
18k 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 ...
0
votes
0answers
23 views

Role of Term Constants in Simply Typed Lambda Calculus [migrated]

In the Wikipedia article on Simply Typed Lambda Calculus (among other places), there is a notion of a "term constant". This is particularly notable in the production grammar given: In this ...
6
votes
0answers
62 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
53 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
107 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
54 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
228 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?
1
vote
0answers
67 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
203 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 ...
2
votes
2answers
201 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
42 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
130 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 ...
0
votes
0answers
38 views

What are some properties of the function that computes the ratio of the first N Jot programs that halt?

Let S(N) be a set of the first N programs in Jot. Suppose that F is function that returns an approximation of the ratio of programs in a set that halt (we can guess ...
2
votes
2answers
172 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
214 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
114 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
345 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
191 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
229 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 ...
13
votes
1answer
296 views

What is the difference between arrows and exponential types in the 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
500 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
151 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
168 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
469 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
159 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
282 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
185 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
371 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
163 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
248 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
254 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 ...
4
votes
2answers
467 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 ...
6
votes
1answer
168 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
158 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
451 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. ...
10
votes
6answers
719 views

What is the point of calling $\lambda$-calculus an algebra?

What is the difference of calling $\lambda$-calculus an algebra instead of a calculus? I raise this question because I read somewhere the line "$\lambda$-calculus is not a calculus but an algebra" ...
-7
votes
1answer
170 views

Lambda Calculus - are these two expressions equivalent? [closed]

(λa.(λb.λc.b)) and (λa.λb.λc.b) I was wondering if someone could explain, using mostly English, what that lambda-calculus expression is supposed to mean, and whether there is any difference between ...
3
votes
2answers
304 views

Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

Normal Order Reduction (NOR) reduce the leftmost, outermost redex. Normal Order Evaluation (NOE) reduce the leftmost, outermost redex, but not within the body of abstractions. So (λw. (λx.x) z) is ...
5
votes
6answers
1k views

Functions that typed lambda calculus cannot compute

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi. As I am a beginner, some reiteration of background information ...
7
votes
1answer
169 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 : ...
1
vote
1answer
300 views

Can “$x(\lambda y.P\;)z$” be $\beta$-reduced?

Consider the untyped $\lambda$-calculus expression $$x(\lambda y.P\;)z$$ ...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've ...
6
votes
1answer
260 views

Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

I'm trying to work through two (non-assessed) class-work questions and am stuck on a question that seems similar to one I could do. The first question was to prove that there does not exist a ...
10
votes
1answer
267 views

Lambda-Calculus terms that reduce to themselves

In my continuing quest to try to learn lambda calculus, Hindley & Seldin's "Lambda-Calculus and Combinators an Introduction" mentions the following paper (by Bruce Lercher) which proves that the ...
5
votes
3answers
421 views

Why does predecessor(zero) need to be zero in Church numerals?

My question may be similar to: Why naturals instead of integers?, but it is more specific. I am trying to learn lambda calculus. All the books make a big deal about how it was necessary that ...
7
votes
2answers
681 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 ...
12
votes
1answer
243 views

Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types). The last step of the proof (page 60), says: "and hence by Lemma 4.1.19(1), ...
13
votes
3answers
478 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
13
votes
4answers
984 views

What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...
6
votes
2answers
261 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 ...