Questions tagged [typed-lambda-calculus]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
0 answers
42 views

Variable opening in locally-nameless representation

Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
phdstudent's user avatar
10 votes
0 answers
209 views

Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?

I am lost in a maze of twisty little type theories, all different. There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the ...
Gro-Tsen's user avatar
  • 619
0 votes
0 answers
29 views

Which family of bicartesian closed functors can define the semantics of simply typed lambda calculus with products and sums

Given any bicartesian closed category $\mathbf{C}$, any natural number $n \geq 0$, and any vector $\boldsymbol{A} \in \mathbf{C}^n$ with $n$ objects $A_1, A_2, … A_n \in \mathbf{C}$, how can I define ...
Johan Thiborg-Ericson's user avatar
-1 votes
1 answer
74 views

What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

I was given an exercise that asked me to assign a simple type to the lambda term: $$ \lambda a.a(\lambda yt.t)(ya) $$ but I couldn't find one, furthermore, the lambda term seems untypable to me ...
Domiziano Scarcelli's user avatar
1 vote
1 answer
82 views

Intuition behind UTT's internal logic

The "internal logic" of type theory UTT is defined in LF as follows: What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
user175254's user avatar
5 votes
2 answers
324 views

Lambda-calculus: Beta-equivalent terms have the same type

In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type? My guess is that I should use the subject reduction, and maybe the ...
Bob's user avatar
  • 381
0 votes
0 answers
89 views

Simple Lambda Calculus Question

For any 2 strongly normalizing terms in the simply typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong ...
Abhishek Manikandan's user avatar
5 votes
2 answers
256 views

Complexity of convertibility in simply typed λ-calculus with sums

For the simply typed λ-calculus with only the function type →, the complexity of deciding βη-equivalence is well-understood: it's TOWER-complete (as mentioned here). I expect the same should be true ...
Lê Thành Dũng Nguyễn's user avatar
1 vote
0 answers
67 views

Interpretation of the degree of a redex

In Girard Proofs and Types, The degree of a type is defined as follows $$\begin{align*}\partial(T_i)&=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\...
Sam Ezeh's user avatar
1 vote
1 answer
86 views

Extension of primitive recursion, that is as powerful as System-T

I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda. I asked myself, if there is a extension of primitive ...
ghostOfTomJoad's user avatar
0 votes
1 answer
102 views

Can we use relational parametricity to simplify the type $\forall a.\,((a\to r)\to a)\to a$ and similar types?

This question is similar to Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$? but looks more complicated. It is about using relational ...
winitzki's user avatar
  • 244
3 votes
1 answer
138 views

Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?

This question is about using relational parametricity to resolve practical questions in pure functional programming in System F. Consider the following types of polymorphic functions: $$ \forall a.\, (...
winitzki's user avatar
  • 244
2 votes
0 answers
144 views

How to implement the next type inference algorithm?

Here I mean only simple typed Lambda calculus / Combinatory logic. Notation: Combinatory logic terms: $F, X_i, Y_i$. Term application: $(F*X_1)$. Type variables $x_i,y_i$. Type assignment: $X:x_i$. ...
Oleg Dats's user avatar
  • 121
10 votes
0 answers
169 views

Stratification of System Fω

I'm wondering if there's any update on this conjecture listed by Urzyczyn from years and years ago (I don't think that's its first appearance), which I'll restate below. System Fω can be stratified ...
ionchy's user avatar
  • 325
1 vote
0 answers
149 views

What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?

The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
jpt4's user avatar
  • 81
2 votes
1 answer
78 views

Question about "Free-ness" of Free SCWF

In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF. My ...
EDJ's user avatar
  • 133
1 vote
1 answer
60 views

Question in relating STLC and Free CCC

In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph) My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
EDJ's user avatar
  • 133
0 votes
1 answer
88 views

Can you always throw away the types when evaluating lambda expressions?

As I understand it, in the simply typed lambda calculus you can type-check your terms, then throw away all the types and do the evaluation exactly as if it was the untyped lambda calculus. Is that ...
azani's user avatar
  • 143
7 votes
0 answers
186 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 ...
Andrew Bacon's user avatar
9 votes
0 answers
202 views

Constructive Strong Normalization of the Extended Calculus of Constructions

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
helmut's user avatar
  • 375
3 votes
2 answers
503 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, ...
Lionel Parreaux's user avatar
2 votes
0 answers
161 views

Set-theoretic encoding of functions in type theory

Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection. In type theory to give a function $A\to B$ is to ...
user avatar
2 votes
1 answer
172 views

Dependent eliminator for empty type in intensional Martin-Löf type theory

In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator. But let's say I'm setting up ...
user avatar
-1 votes
1 answer
102 views

How much type information do Hindley-Milner proof assistants need to remain sound?

A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: $$\forall ...
user1636815's user avatar
1 vote
2 answers
187 views

Explicit type system with infinite non-cumulative universe hierarchy

Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing? I want to ...
user avatar
2 votes
2 answers
151 views

$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$

Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
user avatar
4 votes
1 answer
222 views

Model of MLTT with $\eta$ rule where function extensionality fails

Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?
user avatar
2 votes
1 answer
88 views

Normal term of double negation of W-type

Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle. Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is ...
user avatar
2 votes
1 answer
107 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
5 votes
1 answer
215 views

Is the Mendler-encoding in System-F adequate?

In the paper "Efficiency of Lambda-Encodings in Total Type Theory" it is mentioned that the Church-encoding is adequate and the Parigot encoding is not adequate. This means that any ...
Labbekak's user avatar
  • 701
4 votes
1 answer
478 views

Complexity of type inference in the simply typed lambda calculus

A similar question was answered here: Is simply typed lambda calculus equivalent to primitive recursive functions What I conclude from the answers is that the complexity is that of the extended ...
Yossi Gil's user avatar
  • 481
7 votes
0 answers
234 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
Eric Bond's user avatar
  • 163
10 votes
2 answers
572 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 ...
user1636815's user avatar
-2 votes
1 answer
117 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)\, ...
Joe's user avatar
  • 3
6 votes
1 answer
156 views

What arithmetical theorems can plain $\lambda \Pi$ reason about?

I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}....
bitconfused's user avatar
6 votes
1 answer
230 views

Decidability of rank-k polymorphism vs. System F

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda ...
ionchy's user avatar
  • 325
3 votes
1 answer
195 views

Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
Labbekak's user avatar
  • 701
3 votes
0 answers
166 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-...
fweth's user avatar
  • 139
5 votes
2 answers
259 views

What's the point of stack judgement in CBPV?

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third ...
Qhead's user avatar
  • 53
3 votes
0 answers
395 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: ...
Labbekak's user avatar
  • 701
6 votes
1 answer
317 views

Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
Joey Eremondi's user avatar
6 votes
1 answer
232 views

Structural equality of Pi Types with heterogeneous equality?

I'm trying to implement a proof of the following type: ...
Joey Eremondi's user avatar
7 votes
2 answers
395 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 ...
Labbekak's user avatar
  • 701
11 votes
1 answer
463 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 ...
helmut's user avatar
  • 375
6 votes
2 answers
295 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[...
Joey Eremondi's user avatar
12 votes
1 answer
947 views

Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
Joey Eremondi's user avatar
9 votes
1 answer
470 views

What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus?

This is a reference confusion. Sometimes I see people use the term "Moggi's computational metalanguage" to refer to the calculus presented by Moggi, and sometimes to "Moggi's computational lambda ...
Potter's user avatar
  • 93
3 votes
2 answers
320 views

Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: $$\frac{x: A \vdash a:TB}{x:A \...
Andrew Bacon's user avatar
0 votes
1 answer
55 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 $\...
tci's user avatar
  • 259
10 votes
1 answer
247 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 ...
Martin Berger's user avatar