This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of
mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join
the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
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.
--
RiedelCastro03:45, 1 September 2006 (UTC)reply
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?
--
Thorsten21:39, 28 September 2006 (UTC)reply
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?
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)
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)reply
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)reply
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)reply
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 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)reply
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)reply
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)reply
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:
where is a term constant.
But apparently terms like : are also used in this syntax whereas it's not written in this syntax definition.
Ah, yes, indeed, i didn't realize that ":" are also used in , it's still hard to understand but i'll continue learning, thank you .--
Nicobzz (
talk)
11:49, 26 October 2010 (UTC)reply
I do not have this fresh, but this is incomplete:
Should be something like:
The last rule includes 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: and the conversion rules are constrained to types, for example: , observe that the types resemble modus ponens because
The equation holds in context whenever and . However, if we look at , we have that the type of a.k.a. in this case is not but only . I think a fix should be requiring the type of to be instead.
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 would be typeable. --
Chaosape (
talk)
02:08, 2 January 2017 (UTC)reply
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)reply