tag:blogger.com,1999:blog-11162230.post3472919940521154881..comments2024-03-04T13:50:45.089-08:00Comments on Jeremy Siek: Crash Course on Notation in Programming Language TheoryJeremy Siekhttp://www.blogger.com/profile/13773635290126992920noreply@blogger.comBlogger39125tag:blogger.com,1999:blog-11162230.post-52680555716819710592016-03-12T07:20:48.173-08:002016-03-12T07:20:48.173-08:00Where do you see that notation being used? I don&#...Where do you see that notation being used? I don't recall using it in this blog post... are you referring to some paper?Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-52420664318399192752015-07-31T22:58:21.861-07:002015-07-31T22:58:21.861-07:00Thanks, this is a big help.
But, what does an ov...Thanks, this is a big help. <br /><br />But, what does an overline mean, I know of about 5 different meanings for it, i.e. <br /><br />\left{ \overline{l:x} \right}<br /><br />Also, what do the squiggly arrow, exclamation mark, and at sign mean.<br /><br />thanks muchSzoylent Greenhttps://www.blogger.com/profile/00872620545661065030noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-6416379574994067852014-08-06T19:32:30.225-07:002014-08-06T19:32:30.225-07:00Thanks, fixed that too!Thanks, fixed that too!Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-37647090759800406652014-08-06T16:10:36.051-07:002014-08-06T16:10:36.051-07:00While you're there :-)
Calclus -> Calculus...While you're there :-)<br /><br />Calclus -> Calculusstonesouphttps://www.blogger.com/profile/07065802634885427481noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-87632767295814033552014-03-03T05:20:37.628-08:002014-03-03T05:20:37.628-08:00Yes, a derivation is a proof.
Congruence rules as...Yes, a derivation is a proof.<br /><br />Congruence rules as I discuss above are in TAPL; rules like that appear in every language.<br />Confluence is only briefly discussed in TAPL.Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-45898662221192232282014-03-03T05:16:20.544-08:002014-03-03T05:16:20.544-08:00Thanks, fixed!Thanks, fixed!Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-27366403448183677632014-03-03T05:15:59.225-08:002014-03-03T05:15:59.225-08:00Both EOPL and TAPL are great books, but they are v...Both EOPL and TAPL are great books, but they are very different. EOPL is about understanding programming languages by creating interpreters for them. TAPL is about formalizing the semantics of languages and proving properties about them.Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-35042139498141004432014-02-22T04:45:52.212-08:002014-02-22T04:45:52.212-08:00Hi Jeremy,
Thanks this was a fantastic introducti...Hi Jeremy,<br /><br />Thanks this was a fantastic introduction!<br /><br />Do you have any advice for further reading following on from this post? (Blogs, books etc?)<br /><br />Would you recommend "Essentials of programming languages" or "Types and programming languages" as the next step?<br /><br />Thanks againAnonymoushttps://www.blogger.com/profile/02919360938963587197noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-6079055944182793042014-01-22T02:11:13.263-08:002014-01-22T02:11:13.263-08:00Great post, worth bookmarking. I often get headach...Great post, worth bookmarking. I often get headache with this symbols now I have some place to look, good job.Ajinkyahttp://javarevisited.blogspot.comnoreply@blogger.comtag:blogger.com,1999:blog-11162230.post-71042111349245992192014-01-21T20:40:52.604-08:002014-01-21T20:40:52.604-08:00"I mean, is there something wrong with me for..."I mean, is there something wrong with me for thinking that papers should be written such that any programmer who has enough skills to write a C compiler can understand them?"<br /><br />I don't think this is reasonable; it's rather like saying that papers on quantum mechanics should be readable by anyone who can build a particle accelerator. They're related but not the same. You can write a C compiler and not be conversant with PL theory and terminology. Many of the things you cite as confusing are common knowledge and conventions among computer scientists and mathematicians who study programming languages; it would be very repetitious to include basic explanations and definitions of the field in every paper. Imagine if someone said that every program written in C should be preceded by a set of comments explaining the syntax and semantics of C...Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11162230.post-44771267400653619072014-01-15T09:05:12.863-08:002014-01-15T09:05:12.863-08:00Thank you for this post. It cleared many things in...Thank you for this post. It cleared many things in my head - my mind kept saying 'proves' for ⊢ before. Is there any relationship with a proof, or is this just 'notational coincidence'?<br /><br />I recently got Pierce's TAPL and am working through the first chapters. Are congruence and confluence touched in the text, or should I look for it somewhere else?Anonymoushttps://www.blogger.com/profile/00554220949106409273noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-22412066938514374232014-01-13T03:04:06.598-08:002014-01-13T03:04:06.598-08:00Minor spelling error:
"sytnax-directed"...Minor spelling error:<br /><br />"sytnax-directed" probably should be "syntax-directed" :-)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11162230.post-69813358709736817182014-01-12T00:58:26.475-08:002014-01-12T00:58:26.475-08:00This is great, though there was one bit that is mu...This is great, though there was one bit that is much less obvious to me than all the rest.. " the body of a lambda is checked using the environment from the point of creation (this is lexical scoping) extended with the lambda's parameter". I'm going to think about it some more, as a good exercise. <br /><br />In the example where you demonstrated left-to-right ordering I could easily figure out what the alternative would be, but I don't see how you could write this differently and get a different type of scoping.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11162230.post-22854530586757087742014-01-11T11:15:27.911-08:002014-01-11T11:15:27.911-08:00Thanks. I'm reading Types and Programming Lan...Thanks. I'm reading Types and Programming Languages right now. You're discussing relations then types with the Lambda Calculus. How does the Relational Algebra or Relational Calculus underpinning the relational data model fit into this?Anonymoushttps://www.blogger.com/profile/03971357548186561434noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-59606951636820350102014-01-11T08:09:01.815-08:002014-01-11T08:09:01.815-08:00Thank you for this post! Notations have kept me fr...Thank you for this post! Notations have kept me from reading quite a few papers over the past few months! It's a breath of fresh air to know that nothing in this post went over my head.shashihttps://www.blogger.com/profile/11857005186830809423noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-51177131377890742352014-01-10T17:54:17.200-08:002014-01-10T17:54:17.200-08:00Feel free to write more of these introductory post...Feel free to write more of these introductory posts; I'm more of a compiler guy, and I often get lost when I try to read something about PLT.Vincent Foleyhttps://www.blogger.com/profile/03094490918830336442noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-22475280714910479652014-01-10T15:26:06.248-08:002014-01-10T15:26:06.248-08:00Thanks for this post! It's very helpful! (But ...Thanks for this post! It's very helpful! (But note that lots of stuff disappears if Javascript is disabled.) I recommend amending your introduction to Γ (type environments) with an example so that the remaining 2/3 of the introductory paragraph is easier to understand. I mean, it says "just like Γ" but the reader does not yet have a clear idea of what Γ is.<br /><br />The way small-step semantics works seems weird to me. Although there is a set of rules, it is not necessarily obvious how to apply them. That is, given the rules I suspect it is non-obvious in general how to write a compiler to apply them to an arbitrary input (and it could be especially difficult if the reader does not understand the meaning or purpose of the rules, which tends to happen in these terse PL papers, right?) The example language "e ::= i ∣ −e ∣ e+e" is simple enough that one can figure out how to apply the rules; although I fully understood the language from the start, yet I had to squint my eyes and scratch my head to figure out what was going on with the rules. Oh well, maybe with practice it gets easier. You've shown the derivation of −(2+−5) -> 3, but in general we begin with the input only, and have to determine the output based on the rules. That seems harder... especially if you're not sure what the paper is trying to accomplish. It's not clear to me if the "Eval" relation helps with this problem, maybe you could add a concrete example of an Eval relation?<br /><br />Now here's a paragraph that should be added to half the PL papers in existence:<br /><br />"The x variable ranges over parameter names, such as foo and g. Two expressions right next to each other denote function application (i.e., function call). So if you're familiar with the C language, read e1e2 as e1(e2). In the lambda calculus, functions only take one parameter, so function calls only require one argument. The syntax λx:T.e creates a function with one parameter named x of type T (types will be defined shortly) and whose body is the expression e. (A common point of confusion is to think that x is the name of the function. It instead is the parameter name. The function is anonymous, i.e. it doesn't have a name.) The return value of the function will be whatever the expression e evaluates to."<br /><br />Most papers take big shortcuts, failing to define what "x", "e", etc. mean. Apparently the variables names are supposed to be self-explanatory ("oh, we don't have to say that e is an expression, everyone knows that automatically!") If only PL papers included a link to this blog post, it wouldn't be so bad. But they don't.<br /><br />Another shortcut they'll often take is to define a bunch of operators like have a short definition like "e::= e∆e | e₰e | e e | ..." but with no precedence rules, and then they expect you to know what "a ∆ b c ₰ d" means (even this post uses that shortcut, leaving us to wonder whether "Γ ⊢ e : T" means "Γ ⊢ (e : T)" or "(Γ ⊢ e) : T" (perhaps it is supposed to be obvious, but it's not because there is no independent definition provided for "⊢" and ":"). Sometimes I can't even figure out if some symbol ₹ is a variable or an operator... argh! Even phrases as simple as "T → T" can leave puzzles in the reader's mind, like "oh, does this mean A → A legal but A → B is illegal?"<br /><br />I mean, is there something wrong with me for thinking that papers should be written such that any programmer who has enough skills to write a C compiler can understand them?<br /><br />Conclusion: ranting about PL papers is a lot more fun than reading them. But thanks to this blog post, the job just got easier! Uhhh... of course, those poor souls seaching Google for things like ⊢ and Γ will not actually be able to find this blog post ("your search - ⊢ - did not match any documents.") Oh well.Qwertiehttps://www.blogger.com/profile/04595705428290721343noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-13377525087494497382014-01-10T14:07:40.188-08:002014-01-10T14:07:40.188-08:00Yes. (Not everyone agrees that zero is a natural n...Yes. (Not everyone agrees that zero is a natural number, but PL theorists generally include zero as a natural number.)Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-34957955371386643962014-01-10T10:04:08.948-08:002014-01-10T10:04:08.948-08:00I wish I had had this page when I was studying for...I wish I had had this page when I was studying for my comprehensive exam on PL and type theory. This would have saved a lot of time and unnecessary confusion. Unfortunately a lot of math books assume that everyone knows the notations, or they define the principle notations but not all the details, so articles like this are very useful.Anonymoushttps://www.blogger.com/profile/04367774859096429515noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-81945819305258121552014-01-10T08:57:32.492-08:002014-01-10T08:57:32.492-08:00Is zero (0) in the set of N?Is zero (0) in the set of N?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11162230.post-53710644427895468932012-10-26T12:06:34.257-07:002012-10-26T12:06:34.257-07:00You're very welcome!You're very welcome!Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-41250143939513922122012-10-26T11:37:51.180-07:002012-10-26T11:37:51.180-07:00Thank you very much for this post! This info is wh...Thank you very much for this post! This info is what finally got me through the notation soup in a microsoft research paper on serializing closures in cloud haskell.Anonymoushttps://www.blogger.com/profile/16155471369607312190noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-86806713670208217742012-09-18T12:54:55.235-07:002012-09-18T12:54:55.235-07:00Of course! I was confused with big step. I was eva...Of course! I was confused with big step. I was evaluating the --(5+2) to the final result 7 and erroneously trying to find a rule in your small step semantics to reduce it right away, like you did in the big step version.<br /><br />Thank you very much.Anonymoushttps://www.blogger.com/profile/17378381164437012735noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-19232472193647292032012-09-17T12:38:42.779-07:002012-09-17T12:38:42.779-07:00Dear Aggelos,
Thank you.
Are you asking whether ...Dear Aggelos,<br /><br />Thank you.<br /><br />Are you asking whether the pair (--(5+2), 7)<br />is in the relation -->*? or whether it is<br />in the relation Eval? The answer either way is yes.<br />The following shows that --(5+2) -->* 7.<br /><br />--(5+2) --> --7 --> 7<br /><br />For the big step version (but writing the downarrow as =>), we have<br /><br />5 => 5 2 => 2<br />------------------<br /> 5 + 2 => 7<br />-----------------<br /> -(5 + 2) => -7<br />-----------------<br /> --(5 + 2) => 7<br /><br />Cheers,<br />JeremyJeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-43689725480269310462012-09-17T11:51:20.026-07:002012-09-17T11:51:20.026-07:00Excellent post and great content overall. I would ...Excellent post and great content overall. I would like to ask you something Jeremy. <br /><br />Can a relation (--(5+2), 7) be reduced by your rules? Should we reduce the relation (e,i) simultaneously (and conclude that it cannot be reduced with these rules only) or should we start with the --(5+2) and in three steps ((2)->(3)->(3)) we conclude to 7? <br /><br />I believe that this relation cannot be reduced, but I still feel the need to ask.<br /><br />Thank you,<br />Aggelos <br /><br />Anonymoushttps://www.blogger.com/profile/17378381164437012735noreply@blogger.com