Talk:Simply typed lambda calculus

I started this page, since STL is a central formalism in Theoretical Computer Science. I hope it didn't get too mathematical. I still have to complete the references, if sb else wants to lend a hand, you are very welcome. --Thorsten 21:07, 4 Jun 2005 (UTC)

This is very useful, however, I'm not a mathematician and I don't exactly know what a closed term is and this expression is used twice on the page in places that seem to be important. If I have some time myself I might be able to look it up and fix it but maybe it's easy to be done by someone else. --RiedelCastro 03:45, 1 September 2006 (UTC)

I tried to address this by adding closed terms, i.e. terms typable in the empty context,. I don't know whether this is enough, one could write a whole article about free and bound variables which don't just show up in lambda calculus but also in predicate logic, etc. Maybe there is one already somewhere and we should refer to it? --Thorsten 21:39, 28 September 2006 (UTC)

Shouldn't this page be named "Simply-typed lambda calculus" (hyphen)?

I am usually writing it without a hyphen (but actually use a hyphen between lambda and calculus). Who is using a hyphen between simply and typed?

--Thorsten 19:36, 8 May 2007 (UTC)

According to the Chicago Manual of Style, "simply typed" should not be hyphenated here: "A two-word phrasal adjective that begins with an adverb ending in ‑ly is not hyphenated" (http://www.chicagomanualofstyle.org/16/ch05/ch05_sec091.html)

Enoksrd (talk) 22:23, 7 January 2014 (UTC)

Tait's 1967 paper showed that the equational theory of Gödel's T is a conservative extension of Peano Arithmetic, not the strong normalization of the simply typed lambda calculus, as stated. —Preceding unsigned comment added by 130.226.132.250 (talk) 14:30, 11 September 2008 (UTC)

Type variables -> Base types or Atomic types

Hi. The current presentation talks about "type variables", while in my experience most authors talk about "type constants" or "base types" or "atomic types". I sympathize more with the second terminology — people like Pierce, Girard, Jacobs, Johnstone. The "type variables" terminology seems to be used by Barendregt in his article to clarify the connection with System F, but it is a bit strange because these "variables" don't vary over anything. Any objections if I change "type variables" to "base types"? Also, many of the authors allow some term constants, and product types, in STT. Any objections to mentioning these things? ComputScientist (talk) 13:55, 3 September 2009 (UTC)

I even wrote a stub on type variable with that latter meaning, so yeah, terminology here should be changed. Be WP:BOLD. Pcap ping 14:04, 3 September 2009 (UTC)

You could mention (or detail if you have time) here the "simple extensions" as B.C. Pierce calls them in chapter 11 of his TaPL book. [1] Pcap ping 14:23, 3 September 2009 (UTC)

Another suggestion

The relationship with Type_theory#Simple_theory_of_types should be discussed somewhere in here too. Pcap ping 14:46, 3 September 2009 (UTC)

Typing relation/judgment/derivation

I tried to do a bit of cleaning up of the Semantics section, and also added some description of bidirectional type checking under "Alternative syntaxes". One terminology question/quibble: in Typing rules, I am not sure what distinction you are drawing between "typing relation" and "typing judgment". (I think you are using "relation" where I would use "judgment", and "judgment" where I would use "derivation"...) Could you elaborate? Noamz (talk) 05:46, 26 September 2009 (UTC)

Hi Noamz. My impression is that the "typing relation" is the set of all "typing judgements". That's to say, a judgement is a single triple $(\Gamma ,e,\sigma )$ whereas the typing relation is a set of judgements. A "judgement" is not a "derivation", but the rules let you derive which "judgements" are in the "relation". Do you agree? I think this is what the article says, but do clarify it if poss. ComputScientist (talk) 08:09, 26 September 2009 (UTC)

Okay, I can see how the article says that. I think it would help to add something like, "Instances of the typing relation are called typing judgments. The validity of a typing judgment is shown by providing a typing derivation, constructed using the following rules,..." I'm going to go ahead and add that. Noamz (talk) 17:51, 26 September 2009 (UTC)

Decidability of higher-order matching

The article claims that it is not currently known whether higher-order matching is decidable; however, http://homepages.inf.ed.ac.uk/cps/longmatch.pdf from C. Stirling claims that it is. The article claims for Stirling's work that "the complete version of the proof is still unpublished", but the linked-to paper (from 2009) seems fairly thorough to me. Barring any objection, I'll update the article. Neilc (talk) 07:20, 30 March 2010 (UTC)

A mistake about : The syntax of the simply typed lambda calculus ?

Hello, I'm trying to learn simply typed lambda calculus, and it seems to me to be a mistake if we want to be very rigorous:

it is said that:

The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. The term syntax used in this article is as follows:

$e=x\mid \lambda x:\tau .~e\mid e~e\mid ~c\qquad$ where $c$ is a term constant.

But apparently terms like : $x:\tau$ are also used in this syntax whereas it's not written in this syntax definition.

thank you for what you do.

--Nicobzz (talk) 14:20, 25 October 2010 (UTC)

Hi Nicobzz. I don't think $x:\tau$ is ever used as syntax for a term (in this article). What is written is things like $y:\tau \vdash \lambda x:\sigma .y:\sigma \to \tau$. But this should be bracketed as

$(y:\tau )\vdash (\lambda x:\sigma .y):(\sigma \to \tau )$. There is a ternary relation, $\vdash$, which relates three things: a context, a term, and a type. Does that help? ComputScientist (talk) 20:22, 25 October 2010 (UTC)

Ah, yes, indeed, i didn't realize that ":" are also used in $\Gamma \vdash e:\sigma$, it's still hard to understand but i'll continue learning, thank you .--Nicobzz (talk) 11:49, 26 October 2010 (UTC)

I do not have this fresh, but this is incomplete:

$e::=x\mid \lambda x{\mathbin {:}}\tau .e\mid e\,e\mid c$

Should be something like:

$e::=c:\tau \mid x:\tau \mid \lambda x{\mathbin {:}}\tau .e:\tau \mid e\,e:\tau$

$e::=c:\tau \mid x:\tau \mid (\lambda x{\mathbin {:}}\tau .e:\sigma )\mid (e:\tau \to \sigma )\,(e:\tau )$

$e::=c:\tau \mid x:\tau \mid (\lambda x{\mathbin {:}}\tau .e:\sigma ):(\tau \to \sigma )\mid ((e:\tau \to \sigma )\,(e:\tau )):(\tau \to \sigma )$

$e::=c:\tau \mid x:\tau \mid (\lambda x{\mathbin {:}}\tau .e:\sigma )\vdash (\lambda x.e):(\tau \to \sigma )\mid ((e:\tau \to \sigma )\,(e:\tau ))\vdash (ee):(\tau \to \sigma )$

The last rule includes $\vdash$ which add type inference rules. But mixing inference rules with the syntax of the language seems a dirty way define things. A rule for type generation, and a rule for formula generation is enough for the syntax. the reduction rules: ${\stackrel {\beta }{\rightarrow }},{\stackrel {\eta }{\rightarrow }}$ and the conversion rules are constrained to types, for example: $(\lambda x.e):(\sigma \to \tau )(m:\sigma ){\stackrel {\beta }{\rightarrow }}e\{x\mapsto m\}:\tau$, observe that the types resemble modus ponens $p\rightarrow q,p\vdash q$ because $(\lambda x.e):(\sigma \to \tau )\equiv (\lambda x:\sigma .e:\tau )$

  — Preceding unsigned comment added by 189.178.42.144 (talk) 22:03, 28 December 2015 (UTC) 

Typo

You claim that:

The equation $(\lambda x:\sigma .t)\,u=_{\beta }t[x:=u]$ holds in context $\Gamma$ whenever $\Gamma ,x:\sigma \vdash t:\sigma \to \tau$ and $\Gamma \vdash u:\sigma$. However, if we look at $(\lambda x:\sigma .x)\,u$, we have that the type of $x$ a.k.a. $t$ in this case is not $\sigma \to \sigma$ but only $\sigma$. I think a fix should be requiring the type of $t[x:=u]$ to be $\tau$ instead.

I think there was a mistake, and I think I've fixed it... ComputScientist (talk) 16:02, 2 December 2010 (UTC)

Merge with typed lambda calculus

Should this page be merged with typed lambda calculus?

Duplicate variable names with different types in the typing context.

In the presentation of the inference rules, there should be some words towards avoiding duplicate names with different types in the typing context. Specifically, either renaming of variables that would cause duplicates must be done or the typing context must be given a more detailed treatment to avoid such duplicates. Without doing so, it appears the judgment $\Gamma ,x:\tau _{1},x:\tau _{1}\rightarrow \tau _{2}\vdash xx:\tau _{2}$ would be typeable. --Chaosape (talk) 02:08, 2 January 2017 (UTC)

Alpha equivalence?

I think that the syntax should make it clear that terms are defined up to alpha equivalence. Otherwise the typing rules don't work, for example \x\x.x would not type. — Preceding unsigned comment added by Vasiliscul (talk • contribs) 14:05, 10 September 2018 (UTC)