Questions tagged [lambda-calculus]

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

49 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
20
votes
0answers
1k 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) ...
14
votes
0answers
325 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
13
votes
0answers
240 views

historical question: earliest description of beta-normal terms together with “neutral” terms in lambda calculus?

A bit of "folklore" in lambda calculus is the idea of characterizing the class of $\beta$-normal terms inductively as a syntactic category ($R$) defined in mutual induction with an auxiliary syntactic ...
10
votes
0answers
335 views

Typed Lambda Calculus models and denotations

I'm trying to draw a general mental picture about the models and the denotational semantics of the typed lambda calculus, in its different variants. I'm particularly interested in how the semantics ...
10
votes
0answers
285 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] + \sum_{l=1}^{n-1}\sum_{...
8
votes
0answers
45 views

Relationship between lambda-definability, specification and definability in model theory

I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts: An element $a$ in the domain of a type $A_\sigma$ is ...
8
votes
0answers
147 views

deciding $\beta$-equality of planar lambda terms

Mairson showed that the problem of computing the $\beta$-normal form of a linear lambda term (or equivalently, computing its principal type) is complete for polynomial time. Harry Mairson. Linear ...
8
votes
0answers
263 views

Denotational semantics of System $F_\omega$ with recursive types and general recursion

Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion? I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
8
votes
0answers
82 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
0answers
404 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 ...
8
votes
0answers
176 views

Equivalence of categories of directed complete posets

I asked this question there: https://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 Lambda-...
6
votes
0answers
96 views

Category theory lambda cube?

If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to? https://en.m.wikipedia.org/wiki/Lambda_cube
6
votes
0answers
74 views

Locally-nameless representation: normal order & opening with a bound variable

This question concerns the representation used in Arthur Charguéraud's paper “The locally nameless representation” and is somehow a follow-up on this question, where it is asked about the ...
6
votes
0answers
123 views

Is higher-order unification decidable for terms without abstractions within applications?

Consider the problem of higher order unification - that is, finding a substitution for the equation a = b, where a and ...
6
votes
0answers
299 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 ...
6
votes
0answers
419 views

What is the origin and meaning of the phrase “Lambda the ultimate?”

I've been messing around with functional programming languages for a few years, and I keep encountering this phrase. I understand what lambda means, the idea of an anonymous function is both simple ...
5
votes
0answers
62 views

Semantic read-back of sharing graphs

A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used ...
5
votes
0answers
155 views

Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations $c_1$ and $c_2$ such ...
5
votes
0answers
83 views

Characterisation of the BCIW definable functions

Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.) I ...
4
votes
0answers
98 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
4
votes
0answers
138 views

Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
4
votes
0answers
470 views

Is it possible to derive induction by extending CoC with recursion?

Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms: ...
4
votes
0answers
75 views

Can any Calculus of Construction term be built up from application of a finite number of terms?

Can we form a finite set of well typed calculus of construction terms such that any closed term can be built up from them (plus the type of large types) using only application? I conjecture that the ...
4
votes
0answers
62 views

Finite intersection property of polymorphic type families

Let $\Phi$ be a type functor definable in polymorphic lambda calculus: $$ \alpha : * \vdash \Phi(\alpha) : * $$ $$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$ Suppose further ...
4
votes
0answers
275 views

Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking

I need an extension of System $F_\omega$ with subtyping, and where the variance of type constructors is reflected in their kind. Unfortunately, System $F^\omega_{<:}$, as defined in chapter 31 of ...
4
votes
0answers
192 views

Is it possible to implement tail recursion inside a lambda calculus built on top of functions?

Inside a lambda calculus implementation for ECMASCript 6, we are trying to implement new constructs such as type tags for strong typing, and conditionals such as the ...
4
votes
0answers
62 views

Is the question about closed reduction using token-passing nets still open?

The question about possible implementation of closed reduction using token-passing nets is asked on page 17 in Token-passing Nets for Functional Languages by Jose Bacelar Almeida, Jorge Sousa Pinto, ...
4
votes
0answers
353 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\; ...
3
votes
0answers
106 views

Would it be possible to derive `transp` natively from Path, Interval and typecase?

Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm ...
3
votes
0answers
132 views

Set:Set or Negative Inductives in a Total Language?

In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
3
votes
0answers
86 views

Type System Of $\lambda\mu$-Calculus

reading this paper on CPS-tranformation from the $\lambda\mu$-calculus, I'm a bit confused about the type system presented: Why second-order formulas in the types? Is this according to the Curry-...
3
votes
0answers
85 views

Metrics for modelling convergence in the lambda-calculus

I wonder if there have been efforts to reconcile the measure approach to termination and Scott's domain theory or other topological models of computation. In other words, can we translate this measure ...
3
votes
0answers
119 views

Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example: ...
3
votes
0answers
160 views

Is it possible to check equality of equi-recursive types, or recursive λ-terms?

Can we determine if two λ-terms are equal? Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
3
votes
0answers
84 views

Is there any dataset of lambda terms?

I'm experimenting with optimizing reduction strategies for the untyped lambda calculus. Is there any (publicly available) dataset of (terminating) lambda terms I could use? Maybe it would be ...
2
votes
0answers
45 views

Church numerals and Kleene numerals

Church numerals $\overline{0} = \lambda fx. x$ and $\overline{n} = \lambda f x. f^n x$ are provisions for applying a function $n$ times to an argument. An alternate system of numerals, possibly ...
2
votes
0answers
158 views

Connection between nonmonotonic logic and type theory (lambda calculus)

There is known connection between classical and modal logics and type theory (lambda calculus), but are there connections between nonmonotonic logics (e.g. defeasible logic) and type theory (lambda ...
2
votes
0answers
138 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
0answers
29 views

What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?

I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet. This is what I've thought about ...
1
vote
0answers
37 views

A substitution to add variables in the context

I'm doing type-inference in a dependently typed language, using (as is commonly done) a λ-calculus with explicit substitutions like that of Abadi (with a representation based on debruijn indices) in ...
1
vote
0answers
55 views

Other popular lambda calculus encodings besides Church's?

I know once could start from the popular Church encodings of booleans, ints, etc and arbitrarily obfuscate and complicate them to obtain new representations of the same concepts, but are there other ...
1
vote
0answers
178 views

Is Combinatory Logic (CL) still relevant for programming language theory?

I've been reading up on R. Smullyan's "To Mock a Mockingbird" and Hindley's "Lambda-Calculus and Combinators: An Introduction". I've even read Schonfinkel's 1924 paper introducing the idea of ...
1
vote
0answers
51 views

Effect handlers, arrows and applicatives

After reading Lindley's paper on effect handlers for arrows and applicatives, I got the gist about dynamic and static flow and that it was added to the effect system and so on. However, I do not ...
1
vote
0answers
43 views

Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?

From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from ...
1
vote
0answers
162 views

Optimal reduction using token-passing nets

I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis ...
0
votes
0answers
68 views

Is this a reader monad?

I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where $\alpha$ is any type (I subscript some terms with ...
0
votes
0answers
58 views

Sample Terms in System Omega

I've been implementing mini languages that fall into each corner of the Lambda Cube. My main reference for this has been Types and Programming Languages. The latest one I finished is System Omega. I ...
0
votes
0answers
156 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 ...
-2
votes
1answer
70 views

Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs

Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union. For example, $S$ ...