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

-2
votes
0answers
18 views

Where can integrating the inverse of a function be used in programming application?

Just like [a link]https://en.wikipedia.org/wiki/Fast_inverse_square_root can be used in calculating angle of reflection and incidence in first person shooting games, Where might calculating the ...
2
votes
1answer
128 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
64 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
41 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 ...
12
votes
2answers
342 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 ...
1
vote
1answer
65 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
88 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
51 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
38 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 ...
8
votes
2answers
301 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
46 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 ...
10
votes
3answers
414 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 ...
7
votes
1answer
194 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
56 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
294 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
360 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
164 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 ...
20
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
72 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
565 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
30 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
334 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
314 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
91 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
84 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
136 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
109 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 ...
13
votes
2answers
481 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
146 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
181 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
343 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
341 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
434 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
110 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 ...
6
votes
1answer
669 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
139 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 ...
22
votes
3answers
3k 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 ...
5
votes
1answer
74 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
80 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
164 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
237 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
192 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
146 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
98 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\; ...
17
votes
1answer
199 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
112 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? ...
5
votes
3answers
473 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
83 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 ...
5
votes
2answers
726 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 ...