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.

Filter by
Sorted by
Tagged with
4
votes
0answers
72 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
5
votes
2answers
140 views

Categorical equivalent of higher order logic

From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
6
votes
1answer
163 views

An efficient Beta-Equivalence algorithm?

Is there an efficient algorithm to determine if two terms are beta-equivalent? I'm specifically curious about simply-typed-lambda-calculus, so you can assume both terms are strongly normalizing. I ...
-2
votes
1answer
76 views

Beta reduction and vacuous lambda abstraction [closed]

Suppose we have the following typed lambda term (where $s$ does not occur in E (which is of type $s \to p$) and $s$ and $s'$ have the same type), and want to apply $\beta$-reduction: $(\lambda s. E)\, ...
3
votes
0answers
102 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 ...
1
vote
0answers
36 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 ...
0
votes
0answers
56 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 ...
3
votes
0answers
131 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 (...
5
votes
1answer
234 views

Applications of Barendregt–Geuvers–Klop conjecture

I was learning about type systems from Benjamin C. Pierce's Types and Programming Languages and came across the Lambda cube in the chapter on Higher-Order Polymorphism. After reading up more about it ...
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-...
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 ...
8
votes
1answer
398 views

PHOAS with extrinsic typing?

Parameterized Higher Order Abstract Syntax (PHOAS) is a representation of syntax trees that allows the host language's binding to be used to represent binding in the language being modelled, while ...
3
votes
0answers
73 views

Topologies for modelling divergence in the lambda-calculus

I wonder if there exist topologies for the lambda-calculus where computational divergence (like for $\Omega = (\lambda x. x x) (\lambda x. x x)$) has a topological meaning as the divergence of a ...
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 ...
5
votes
0answers
61 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 ...
3
votes
0answers
114 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: ...
7
votes
2answers
249 views

Termination checking for Scott-encodings in System F with positive-recursive types

Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types. All papers I have found use languages with constructors and case analysis (for example ...
3
votes
1answer
101 views

Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence

In Sorensen and Urzyczyn's book there is a lemma (1.3.11) which I am having a hard time proving. 1.3.11 Lemma: If there is an infinite $\beta \eta$-reduction sequence starting with a term $M$ then ...
1
vote
0answers
165 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 ...
10
votes
1answer
933 views

What is the “question” that programming language theory is trying to answer?

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
1
vote
1answer
67 views

Extending EAL with recursion makes it incompatible with the abstract algorithm?

A few years ago, I've asked if Elementary Affine Logic can be used as the core type system of a practical programming language. The accepted answer argues that, yes, although such language would be ...
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 ...
3
votes
0answers
155 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, ...
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 ...
7
votes
3answers
337 views

When a type is a value?

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
3
votes
1answer
223 views

Busy Beaver Equivalent for the Untyped Lambda Calculus

In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus: Over all terms in the ULC composed of ...
11
votes
2answers
360 views

Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
9
votes
1answer
241 views

Understanding the Proof of Strong Normalization of the Calculus of Constructions

I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong ...
5
votes
2answers
233 views

Typing of substitution in a bidirectional type system

In most typed lambda calculi, we have the following lemma: If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
5
votes
2answers
330 views

Preservation under Substitution with Telescopes

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution": If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$, then $\Gamma \...
6
votes
0answers
71 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 ...
11
votes
3answers
657 views

Equivalent formulation of complexity theory in Lambda Calculus?

In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched. ...
4
votes
1answer
114 views

Is the church-style affine calculus of constructions with unrestricted recursion consistent?

Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example: ...
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 ...
11
votes
5answers
435 views

Representing bound variables with a function from uses to binders

The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
4
votes
1answer
202 views

Why isn't it “enough” to prove induction with one extra “INat” argument?

It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is, ...
5
votes
1answer
1k views

Is a CEK machine an implementation of a CESK machine?

We know that a CESK machine can be defined as: a state-machine in which each state has four components: a (C)ontrol component, an (E)nvironment, a (S)tore and a (K)ontinuation. One might imagine ...
7
votes
1answer
184 views

If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?

Question If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ...
6
votes
2answers
147 views

Is it possible to create a “quote” function that, given a native λ-term, returns its λ-encoded representation?

Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices: ...
7
votes
1answer
367 views

Fixed points in dependent type theories

Most dependent type theories aim for some notion of correctness in two respects: The type system must be decidable. The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
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 ...
1
vote
1answer
111 views

What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?

Let $\Lambda$ be a set of strongly normalizing lambda terms. Let $\mathtt{NF} : \Lambda \rightarrow \Lambda$ be evaluation to the normal form. Let $ \lvert x\rvert : \Lambda \rightarrow \mathbb{N}$ be ...
1
vote
0answers
50 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 ...
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 ...
0
votes
1answer
49 views

Head variables of terms after application

We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\...
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 ...
1
vote
1answer
138 views

How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?

Suppose that we take the Calculus of Constructions as a basis, but take away exponential functions (allowing only linear functions), and add the controlled duplication rules of EAL. That'd, I believe, ...
10
votes
1answer
213 views

Program inversion algorithms for higher-order programs

The term program inversion has multiple shades of meaning, but probably got started with J. McCarthy's 1956 work The Inversion of Functions Defined by Turing Machines in the context of AI. By now ...
7
votes
1answer
324 views

Finding a common factor in $\lambda$-terms that agree under certain substitutions

Suppose that $\mathcal{L}$ is the language of a simply typed lambda calculus of two base types, $e$ and $t$, with infinitely many constants at each type. A substitution $j$ is a mapping from ...

1
2 3 4 5