The syntax STLC is usually written:

$e ::= x |\lambda x : \tau . e|(e \space e)|c$

However, the application rule appears to accept all expressions on the left hand side. Shouldn't the application rule be written:

$(\lambda x : \tau . e \space e : \tau)$ ?

The only time an application makes sense both intuitively and type-wise is by reducing and abstraction by replacing its variable with an expression. All other cases would be:

$(x \space e)$ makes no sense. By the time application can take place x will be substituted with its bound expression. By this logic it will be either an abstraction, as labeled okay above or something else, discussed below

$(c \space e)$ again, you can't apply to a value.

$((e \space e) \space e)$ this is not an issue because applications resolve to an expression, and following that recursive logic it will resolve to one of the aforementioned cases.


Shouldn't the application rule be written:

$(\lambda x : \tau . e \space e : \tau)$ ?

No, there are at least three problems with this formulation:

  • First, it is important that the first time can be a variable. For example, we want to allow the term $$ x \; y $$ Why do we want to allow this? Well we want to be able to apply a function to an argument. For example, the following lambda term is a function which applies $x$ to $y$: $$ \lambda x: \tau_1 \to \tau_2. \lambda y: \tau_1. (x \; y) $$

  • Second you are assuming the first term has already been reduced. This is not generally true. Although once reduced, the term $e_1$ in $(e_1 \; e_2)$ should usually be a lambda expression (or a variable), this may not hold before it has been evaluated.

  • The third problem is really a misunderstanding, not a concrete issue with your formulation: in STLC, we allow terms that are not well-typed. For example, if there are base types including numbers and Booleans, then we can write nonsense like $$ \text{true} \; 3 $$ and this is a valid lambda term, just not a well-typed one. So your question seems to want to make sure that the application rules is well-typed, but that will be part of the typing rules, not part of the definition of a lambda term itself.

The only time an application makes sense both intuitively and type-wise is by reducing and abstraction by replacing its variable with an expression.

That is correct, and this is going to be the motivation for the typing rules. In fact, the typing rule will say this exactly: the term $e_1 \; e_2$ will be well-typed only if $e_1$ is a function $\tau_1 \to \tau_2$ and $e_2$ is a value of type $\tau_1$. But for the reasons above, it is important that these restrictions be on the typing level, not baked into the syntax.

$(x \space e)$ makes no sense.

It does make sense: but only in a context where $x$ is a variable of a function type. Think of a variable that may be assigned to a value; if it is assigned to a value which is a function, then this makes sense.

$(c \space e)$ again, you can't apply to a value.

It's true that this makes no sense, but we allow it anyway; we just don't say that it is well-typed.

$((e \space e) \space e)$

As you said this case may resolve to one of the other cases, but we are defining the syntax here, not the semantics. So it doesn't imply that we should rule it out just because resolves to the other cases; it is still a valid lambda term, just one that is not fully reduced.

  • $\begingroup$ So if I change the rule to read the l.h.s must be a function type, which is equivalent to lambda abstraction but at least allows the rule for bound function type variables, and postulate that I only care about well typed expressions, then it holds true? (Additionally defining the semantics of parsing to collapse applications left to right and inwards to outwards). This dialect is of course no longer usefully called STLC, but does it lose any computational complexity? $\endgroup$ – Stegosaurus Apr 9 '20 at 2:51
  • $\begingroup$ @Stegosaurus That would not make sense. You can't bake into the definition of the language that the terms have already been fully evaluated. You need to allow that $e_1$ has not been fully reduced in $(e_1 \; e_2)$. Besides this restricting to well-typed expressions still allows $e_1$ to be a variable which you seem to not want to allow. $\endgroup$ – 6005 Apr 9 '20 at 3:57
  • $\begingroup$ can I enforce the function type of the left expression? And I know I cant enforce full evaluation in the language, but I can enforce it as a dialect when also defining the semantics and parsing laws of the language. I'm taking a more holistic view of the computations that occur $\endgroup$ – Stegosaurus Apr 9 '20 at 12:08
  • $\begingroup$ @Stegosaurus You can enforce the function type (that's what STLC does) but not the function syntax (lambda expression). Consider the first example in my answer of $\lambda x. \lambda y. (x \; y)$. if you try to "enforce it as a dialect" as you say, then you would disallow that computation. I think you are still mixing up syntax and semantics. The reason we need to keep them separate is in order to get all possible functions (like the first one in my answer). $\endgroup$ – 6005 Apr 9 '20 at 12:22
  • $\begingroup$ so is the rule $(e_1 : \sigma \to \tau \quad e_2 : \sigma ) : \tau$ a valid restriction only allowing fully reducible expressions? $\endgroup$ – Stegosaurus Apr 9 '20 at 16:06

No, because there are terms of function type $\sigma \to \tau$ which are not $\lambda$-abstractions, and neither is it true that every term of type $\sigma \to \tau$ is equal to a $\lambda$-abstraction – consider a variable of type $\sigma \to \tau$.

It is true that every closed term of function type normalizes to a $\lambda$-abstraction, but that is quite irrelevant and plays no importance when we postulate general rules that should work on all rules. You are attempting to mix the structural rules governing $\lambda$-calculus with theorems about it that cannot be proved without first having such structural rules available in full generality.

  • $\begingroup$ Can you please give an example of an arrow type that cannot be expressed as a lambda abstraction? $\endgroup$ – Stegosaurus Apr 9 '20 at 12:12
  • $\begingroup$ Additionally, could $(e_1:\sigma \to \tau \space e_2 : \sigma ) : \tau $ be used to enforce well typed application? $\sigma$ may be any type, including arrow types. Instead of saying that the l.h.s. should be a lambda abstraction, I am using type rules to do the enforcement $\endgroup$ – Stegosaurus Apr 9 '20 at 12:20
  • $\begingroup$ You probably are asking for an expression of an arrow type that is not equal to a $\lambda$-abstraction. The slopiness in your phrasing worries me, as it possibly indicates some underlying confusion about what is what. Sure, $f : \sigma \to \tau \vdash f : \sigma \to \tau$, i.e., a variable $f$ of type $\sigma \to \tau$ is not equal to a $\lambda$-abstraction. $\endgroup$ – Andrej Bauer Apr 9 '20 at 19:36
  • $\begingroup$ @AndrejBauer technically, with the $\eta$ rule, every variable with a function type is convertible to a $\lambda$. In an algebraic specification for STLC, we could add a condition that an applied term must be a $\lambda$, and that wouldn't change anything. $\endgroup$ – András Kovács Apr 10 '20 at 7:23
  • $\begingroup$ @AndrásKovács: good point. I'll leave it to you then to convince the OP that what they're asking for is not a good idea :-) Ok, how about this: the typing rules should not depend on whether we have an $\eta$-rule. (But why?) $\endgroup$ – Andrej Bauer Apr 10 '20 at 8:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.