Questions tagged [typed-lambda-calculus]
The typed-lambda-calculus tag has no usage guidance.
37
questions
-2
votes
0answers
39 views
Simply typed lambda calculus with single type Unit
I have a question that I can't solve:
Given the simply typed lambda-calculus with call-by-value evaluation and the regular inference rules for abstraction, application and variables. If I just add ...
5
votes
2answers
134 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 ...
3
votes
0answers
72 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:
...
6
votes
1answer
225 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 ...
6
votes
1answer
154 views
Structural equality of Pi Types with heterogeneous equality?
I'm trying to implement a proof of the following type:
...
6
votes
2answers
168 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 ...
9
votes
1answer
190 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
210 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[...
10
votes
1answer
442 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 ...
8
votes
1answer
171 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 ...
2
votes
2answers
214 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 \...
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 $\...
10
votes
1answer
193 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
320 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 ...
11
votes
3answers
250 views
Calculus of Constructions: compress expression to its smallest form
I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient ...
12
votes
1answer
164 views
Eta expansion in the pattern lambda calculus
Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.
http://www.sciencedirect.com/science/article/pii/S0304397508000571
In some sense, a pattern is a tree of variables ...
2
votes
1answer
577 views
Is simply typed lambda calculus equivalent to primitive recursive functions
It's well known that the computation models untyped lambda calculus and $\mu$-recursive function are equivalent in terms of computability (in fact they are both Turing complete.) It is also well known ...
4
votes
0answers
72 views
Coherence spaces and full completeness for the implicative fragment of linear logic
Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$.
I ...
5
votes
1answer
221 views
Recursive types and the empty type
In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126)....
5
votes
1answer
105 views
Inference in typed lambda calculus theories
I'd like to do automated inference, say solving word problems or reducing to normal form, in an equational theory of the typed lambda calculus (with product and unit types). Equivalently, in category-...
5
votes
1answer
222 views
Type checking, Hypothetical judgments, meaning explanations and computational type theory
We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). ...
3
votes
1answer
361 views
Does the simply typed lambda calculus have general iteration?
In more expressive calculi such as System F, the Church numerals, by virtue of their design, allow for iteration over an arbitrary type. Can this effect be replicated in the simply typed case?
To be ...
5
votes
0answers
81 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 ...
3
votes
1answer
283 views
Enumerating all simply typed lambda terms of a given type
How can I enumerate all simply typed lambda terms which have a specified type?
More precisely, suppose we have the simply typed lambda calculus augmented with numerals and iteration, as described in ...
8
votes
0answers
237 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]...
21
votes
2answers
3k views
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
2
votes
0answers
153 views
Heyting algebra in simply typed lambda calculus
The Emil Jeřábek's comment in Can boolean algebra be expressed in simply typed lambda caclulus? give rise to the following question:
Can some non-trivial Heyting algebra be expressed in simply typed ...
3
votes
1answer
132 views
What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type.
Particularly, the only ...
1
vote
1answer
109 views
Observational Equivalence of open terms in PCF
The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms.
Lets consider the simple case where the terms ...
3
votes
0answers
51 views
Functionality of a hierarchy of definable functions over $\mathbb{N}$
Let $T$ be the complete hierarchy of functions over $\mathbb{N}$. That is: $T$ = $\bigcup T_{\tau}$ for all simple types $\tau$ built up from the basic type $\mathbb{N}$, with $T_{\mathbb{N}} = \...
4
votes
1answer
121 views
Rendering of type-level computation
Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some ...
20
votes
2answers
1k 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 ...
21
votes
3answers
1k 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 ...
5
votes
1answer
210 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 ...
11
votes
1answer
569 views
Simply typed lambda calculus and higher order logic
What is the relation between simply typed lambda calculus and higher order logic?
Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related ...
4
votes
1answer
220 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
&\vdash\bot\...
16
votes
1answer
2k 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 can ...
