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
2 votes
0 answers
42 views

Is there a standard way to "point" at subterms in a lambda expression?

Let's say I have a lambda expression $$ (\lambda x . (\lambda w.ww)x) y $$ There are a bunch of subterms: $(\lambda x . (\lambda w.ww)x) y$ $\lambda x . (\lambda w.ww)x$ $(\lambda w.ww)x$ $\lambda w ....
user avatar
  • 123
4 votes
1 answer
100 views

What are the application of Scott-Topology in theoretical computer science?

During a work I came across the Scott-Topology and I see that Scott-continuous functions show up in the study of models for lambda calculi. What I cannot understand is how this enrich the lambda-...
user avatar
  • 49
3 votes
0 answers
84 views

Call-by-value solvability

Background There are two fairly common definitions of solvability. The general one states that the term can be used to get any chosen result (i.e. normal form):$$T\text{ solvable} \overset{\text{def}}{...
user avatar
  • 521
7 votes
0 answers
94 views

What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the ...
user avatar
1 vote
1 answer
146 views

Intuitive way to handle variable binding

Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ...
user avatar
3 votes
0 answers
62 views

Expressive power of lambda-calculus with restricted application

Consider a syntactic restriction of the (untyped) $\lambda$-calculus in which an application cannot have another application as an immediate subterm. More precisely, restricted terms ($R,S,...$) and ...
user avatar
  • 653
2 votes
0 answers
57 views

Are there any references for this theorem of Lercher?

Let $\Delta = \lambda x.(x)x$ and consider $\Omega = (\Delta)\Delta$. Then $\Omega$ is exactly the only $\lambda$-term of the form $(\lambda x.t)v$ such that $(\lambda x.t)v=t\{v\ /\ x\}$. Does ...
user avatar
  • 121
5 votes
1 answer
83 views

Can a normal form term be extensionally equivalent to a term with no WHNF?

For convenience I'm using using the combinators SKIBCMTV I notice that it's possible to have a normal-form term extensionally equivalent to a term which has no normal form: ...
user avatar
  • 916
0 votes
0 answers
135 views

What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?

There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...
user avatar
  • 3,045
7 votes
0 answers
126 views

Are the non-lazy / non-weak semantics of the $\lambda$-calculus related to weak evaluation?

Vague question The most common semantics of the call-by-name $\lambda$-calculus (Hyland/Wadsworth’s observational equivalence $\approx_\text{HNF}$ and Morris’s observational equivalence $\approx_\text{...
user avatar
  • 521
1 vote
0 answers
88 views

Is there some n such that lambda calculus with only n variables is Turing-complete?

Typically in lambda calculus you have an infinite stock of variables. Could we get away with a finite set?
user avatar
7 votes
0 answers
168 views

$\lambda$-definability and structure preserved by homomorphisms

I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it. Some prelimary definitions. A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
user avatar
3 votes
1 answer
156 views

Fixed points of fixed-point combinator?

A fixed point f of a fixed-point combinator would be a function that has itself as a fixed point: f(f) = f. The only such ...
user avatar
5 votes
1 answer
118 views

$\eta$-reduction not locally confluent on well-typed terms

This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]." [20] is a reference to a 300-page book with no further details and ...
user avatar
  • 61
8 votes
0 answers
172 views

What is the "standard" lambda-calculus model for bicartesian closed categories?

(I'm familiar with the lambda-calculus, less so with its categorical models.) It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
user avatar
  • 1,872
2 votes
1 answer
185 views

Alternatives to Normalization by Evaluation

Reading about lambda calculus I got the impression that normalization is evaluation. So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel). ...
user avatar
  • 29
3 votes
2 answers
305 views

Are there strongly normalizing lambda terms that cannot be given a System F type?

I know that all well-typed System F terms are strongly normalizing, but is the converse true as well? In other words, does System F typeability precisely characterize program termination? (And if so, ...
user avatar
2 votes
1 answer
98 views

Typing inference as a map on abstract syntax trees

Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-...
user avatar
3 votes
0 answers
99 views

CCCs, computational calculi and point-surjectivity

The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $U$ that has some relationship to its exponential object $U^U$ e.g. a retraction ...
user avatar
3 votes
1 answer
138 views

Structural normalization algorithm for the simply typed lambda calculus

I would like to know if there is a (piecewise) structural normalization algorithm for the simply typed lambda calculus. By structural I mean a recursive function that only calls itself on subterms of ...
user avatar
  • 165
1 vote
0 answers
38 views

Nominal Tree Languages i.e. with Binders and Infinite Symbols?

I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence. I've found so far: ...
user avatar
2 votes
1 answer
123 views

Phonology and lambda calculus

I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
user avatar
5 votes
0 answers
144 views

Applications of solvability in the λ-calculus

What are applications of solvability / unsolvability, and of operational characterizations of solvability? Solvability In the (untyped pure call-by-name) $\lambda$-calculus, a closed term is said to ...
user avatar
  • 521
15 votes
1 answer
903 views

Can we derive Cubical Type Theory from Self-Types?

Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
user avatar
  • 3,045
1 vote
0 answers
68 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 ...
user avatar
  • 119
-2 votes
1 answer
78 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$ ...
user avatar
  • 105
0 votes
0 answers
83 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 ...
user avatar
  • 105
6 votes
0 answers
158 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
user avatar
  • 153
5 votes
2 answers
233 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.
user avatar
  • 737
9 votes
2 answers
401 views

Is there an efficient beta-equivalence algorithm?

Is there an efficient algorithm to determine if two terms are beta-equivalent? Specifically, I am curious about simply-typed-lambda-calculus, so you can assume both terms are strongly normalizing. I ...
user avatar
-2 votes
1 answer
105 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)\, ...
user avatar
  • 3
3 votes
0 answers
123 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 ...
user avatar
  • 3,045
1 vote
0 answers
52 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 ...
user avatar
  • 382
3 votes
0 answers
150 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 (...
user avatar
5 votes
1 answer
383 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 ...
user avatar
  • 151
3 votes
0 answers
118 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-...
user avatar
  • 139
1 vote
0 answers
60 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 ...
user avatar
8 votes
1 answer
478 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 ...
user avatar
3 votes
0 answers
115 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 ...
user avatar
  • 737
2 votes
0 answers
54 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 ...
user avatar
  • 113
7 votes
1 answer
94 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 ...
user avatar
3 votes
0 answers
291 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: ...
user avatar
  • 691
7 votes
2 answers
334 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 ...
user avatar
  • 691
3 votes
1 answer
168 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 ...
user avatar
2 votes
0 answers
378 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 ...
user avatar
  • 5,157
12 votes
1 answer
2k 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 ...
user avatar
  • 5,157
1 vote
1 answer
83 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 ...
user avatar
  • 3,045
4 votes
0 answers
106 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 ...
user avatar
3 votes
0 answers
260 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, ...
user avatar
  • 3,045
4 votes
0 answers
150 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 ...
user avatar

1
2 3 4 5