# Tag Info

83

An excerpt from History of Lambda-calculus and Combinatory Logic by F. Cardone and J.R. Hindley(2006): By the way, why did Church choose the notation “$\lambda$”? In [Church, 1964, §2] he stated clearly that it came from the notation “$\hat{x}$” used for class-abstraction by Whitehead and Russell, by first modifying “$\hat{x}$” to “$\wedge x$” to ...

63

Ironically, the title is on point but not in the way you seem to mean it which is "is the lambda calculus just a notational convention" which is not accurate. Lambda terms are not functions1. They are pieces of syntax, i.e. collections of symbols on a page. We have rules for manipulating these collections of symbols, most significantly beta reduction. You ...

51

It's inspired from real events, but the way it's stated is barely recognizable and “should be regarded with suspicion” is nonsense. Consistency has a precise meaning in logic: a consistent theory is one where not all statements can be proved. In classical logic, this is equivalent to the absence of a contradiction, i.e. a theory is inconsistent if and only ...

30

I haven't read this anywhere, but this is how I believe $Y$ could have been derived: Let's have a recursive function $f$, perhaps a factorial or anything else like that. Informally, we define $f$ as pseudo-lambda term where $f$ occurs in its own definition: $$f = \ldots f \ldots f \ldots$$ First, we realize that the recursive call can be factored out as ...

29

Certainly, assigning a type to $\lambda x. x\ x$ is not enough for inconsistency: in system $F$, we can derive $$\lambda x.x\ x:(\forall X.X)\rightarrow (\forall X.X)$$ in a pretty straightforward way (this is a good exercise!). However, $(\lambda x.x\ x)(\lambda x.x\ x)$ cannot be well typed in this system, assuming $\omega$-consistency of 2nd order ...

24

The main theorem regarding this issue is due to a British mathematician from the end of the 16th century, called William Shakespeare. His best known paper on the subject is entitled "Romeo and Juliet" was published in 1597, though the research work was conducted a few years earlier, inspired but such precursors as Arthur Brooke and William Painter. His main ...

24

There are many reasons why the lambda calculus is so important. A very important reason is the lambda calculus allows us to have a model of computation in which computable functions are first-class citizens. One cannot express higher-order functions in the language of middle school algebra. Take as example the lambda expression $$\lambda f. \lambda g. \... 23 In a nutshell: What characterizes imperative programming languages as close to Turing machines and to usual computers such as PCs, (themselves closer to random access machines (RAM) rather than to Turing machine) is the concept of an explicit memory that can be modified to store (intermediate results). It is an automata view of computation, with a concept ... 21 Turing-complete is just a name. You can call it Abdul-complete if you want. Names are decided upon historically and are often named after the "wrong" people. It's a sociological process that has no clear criteria. The name has no meaning beyond its official semantics. Imperative languages are not based on Turing machines. They are based on RAM machines. ... 20 What research have you done to answer that question? I just plugged it as it is in Google, and got as second answer (the first may be as good, I did not check) a reference to a section of a bible on your topic: Hal Abelson's, Jerry Sussman's and Julie Sussman's Structure and Interpretation of Computer Programs (MIT Press, 1984; ISBN 0-262-01077-1), aka the ... 19 Sure, this is a standard encoding exercise. First of all, let p : \mathbb N^2 \to \mathbb N any bijective computable function, called a pairing function. A standard choice is$$ p(n,m) = \dfrac{(n+m)(n+m+1)}{2}+n $$One can prove that this is a bijection, so given any natural k, we can compute n,m such that p(n,m)=k. To enumerate lambda terms, ... 17 The term you are reducing is (K_y \Omega) where K_y is the constant function \lambda x. y (it always returns y, ignoring its argument) and \Omega = (\lambda x. (x \, x) \: \lambda x. (x \, x)) is a non-terminating term. In some sense \Omega is the ultimate non-terminating term: it beta-reduces to itself, i.e. \Omega \to \Omega. (Make sure to ... 16 There are four main approaches, though these only scratch the surface of what is available: via lambdas and records: the idea is to encode objects, classes and methods in terms of more traditional constructs. Benjamin Pierce's work from the mid 90s is representative of this approach. Abadi and Cardelli's object calculi (see Abadi and Cardelli's book A ... 16 In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type \forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta, but there is a term of type \... 16 In traditional Martin-Löf type theory there is no distinction between types and propositions. This goes under the slogan "propositions as types". But there are sometimes reasons for distinguishing them. CoC does precisely that. There are many variants of CoC, but most would have$$\mathsf{Prop} : \mathsf{Type} but not $\mathsf{Type} : \mathsf{Prop}$. ...

15

My favourite example of a context-sensitive language (CSL) is SAT. The Landweber-Kuroda Theorem says that CSL = NSPACE$[n]$. Any SAT instance has a linear-size certificate, so SAT is a CSL. See my question Context-sensitive grammar for SAT? for references and discussion. Many other NP-hard languages are also in CSL by the same reason, such as CLIQUE. ...

15

Context are used for many purposes, but typically to define congruences on programs. Evaluation contexts are a subset of contexts. They are typically used to define reduction relations. Let me give an example of each. One formal way of defining program equality is to say two programs $M$ and $N$ are contextually equal they can replace each other in each ...

15

A context is a syntactic notion. A context is a term with one hole in it. (Occasionally there are multi-hole contexts, the definition will be given clearly in that case.) The syntax of contexts is defined by taking the syntax of terms and allowing one subterm to be a hole $[]$ instead of a term. In BNF (I use the lambda-calculus as an example, without ...

14

So what is the equivalent for object oriented languages? Lambda calculus. I mean, there is Cardelli's object calculus (and a handful of derivatives), but in general, there's nothing fancy about object oriented languages that requires a new approach to computation. It's well known (see TaPL for example) how to extend/encode Records and Mutation (and sub-...

14

Consider the terms of the $S,K_2,I$ calculus as trees (with binary nodes representing applications, and $S, K_2$ leaves representing the combinators. For example, the term $S(SS)K_2$ would be represented by the tree @ / \ / \ @ K2 / \ / \ S @ / \ / \ S S To each tree $T$ associate its ...

13

In computer science we want to analyze and understand source-code with mathematical rigour. That's the only way to prove interesting properties (such as termination) with absolute certainty. For that we need a language with a very well-defined meaning for every construct. In theory this could be any language with a good formal semantics. But to make things ...

13

Pairs This encoding is the Church encoding of pairs. Similar techniques can encode booleans, integers, lists, and other data structures. Under the context x:a; y:b, the term pair x y has the type (a -> b -> t) -> t. The logical interpretation of this type is the following formula (I use standard mathematical notations: $\to$ is implication, $\vee$ ...

13

This is a known problem, known as Higher Order Unification. Unfortunately, this problem is undecidable in general. There is a decidable fragment, known as Miller's Pattern Fragment. It's used extensively in, among other things, typechecking of dependently-typed programs with metavariables or pattern matching. This fragment is where unification variables are ...

12

Apologies in advance for the shameless plug, but there is a paper of mine on a quantum lambda calculus that you may find interesting. It is called The Dagger Lambda Calculus and provides a higher-order representation for the diagrammatic circuits that the categorical school of quantum computation have introduced: http://arxiv.org/abs/1406.1633 You can also ...

12

The connection between object model core and set theory is described in the following documents: Object Membership: The Core Structure of Object Technology Object Membership – Basic Structure What Is a Metaclass? The documents present the structure of instance and inheritance relations between objects. Such a structure can be considered the highest ...

12

All proofs of the equivalence of these two models of computation are constructive, that is they describe an algorithm for converting a program from one model of computation to the other. However, I caution you that these proofs are probably rather informal, and may not satisfy you. You may get luckier if you consult original work by computing pioneers (...

12

It helps to remember that $\forall$ (or $\Pi$ as you sometimes see) is a type. It's generalizing $\to$. So while it makes perfect sense to say $(\lambda x : A. M)\ N$, it doesn't make sense to say $(\forall x : A. M)\ N$ because $\forall ...$ is just a type. You wouldn't say $(A \to B)\ N$ becaues $\to$ isn't for computing per-se, it's there to classify ...

12

Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.

11

As Yuval has pointed out there is not just one fixed-point operator. There are many of them. In other words, the equation for fixed-point theorem do not have a single answer. So you can't derive the operator from them. It is like asking how people derive $(x,y)=(0,0)$ as a solution for $x=y$. They don't! The equation doesn't have a unique solution. Just ...

Only top voted, non community-wiki answers of a minimum length are eligible