I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
https://en.wikipedia.org/wiki/Gymnasium_(school)
> I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
https://en.wikipedia.org/wiki/Gymnasium_(Germany)
And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof.
It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs.
> I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course.
A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations?
They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
I've never heard of "sequent calculus" before, and I don't expect anyone I know to have heard it. Apparently it's not calculus.
> They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
I don't think universities are watered down because they don't teach notation that most people don't know and find obscure. My university is famous for a difficult admissions process, tough courses that most people only learn 2/3 of the material, and grading curves calibrated so getting 60% on exams is enough for a B or A.
----
https://en.wikipedia.org/wiki/Sequent_calculus
Wikipedia says "Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments."
I didn't learn "every statement is conditional" logic involving turnstiles, I learned something where the assumptions were given in the problem, and each line was proven based on the previous lines, which boiled down to the initial givens.
It's also not particularly difficult to pick up. We teach basic sequent calculus proofs to high schoolers in our summer program. If you can follow the two column proofs from high school geometry, then you can follow the notation used in standard programming language texts and papers.
I mean, what's why I said almost?
> It's also not particularly difficult to pick up.
Well, what I said was from personal experience, so maybe I'm just dumb... I'm not sure what else to tell you. Never in my life had so much of my continual struggling with a technical topic been solely due its pointlessly convoluted notation and roundabout communication as it had with PL theory.
Some things are difficult to learn without a good teacher. New notation is probably toward the top of that list. And there's really no way to study something like type systems without inventing some sort of notation. You can go back and read early papers in mathematical logic before the notation was invented. They take pages upon pages to communicate very simple things.
[1] https://www.google.com/books/edition/Advanced_Topics_in_Type...
It's a coincidence, because I was just reading that chapter on pure type systems earlier today. Yes, I understand that notation. FWIW those aren't proofs; those are typing rules.
The top-left rule on page 52 says that given that:
- In context Gamma, T1 = T2 where both have kind *
- If x : T1 is added to the context Gamma, K1 = K2
you can derive that in context Gamma, (x : T1) -> K1 = (x : T2) -> K2.
A context is just a symbol table mapping names to types. Conventionally, uppercase gamma or uppercase delta is used.
The uppercase pi is just another way of writing the dependent function type. If you think of types algebraically, dependent function types are similar to repeated multiplication, which use capital pi. It's similar to how summation uses capital sigma (and therefore the dependent sum type uses capital sigma as well).
Gamma |- exp : A
This is a common pattern that says that exp has type A when the contents of Gamma are in scope.
Gamma |- exp1 = exp2 : A
This is a common pattern that says that exp1 and exp2 are equal terms of type A when the contents of Gamma are in scope.
I've found that most type system rules follow the same format more or less.
Sometimes, I do misread things. (When reading the page you linked, at first I mistook T1 = T2 for a type of kind *, then I realized I misunderstood it.)
-> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.
Frankly, I'd expect any CS student at a decent university to be able to parse that page fairly easily.
Dismissing this foreign language aspect as easy to learn doesn't get to the heart of the matter. Is it really too much to be ask to be taught in vernacular English rather than foreign Church Latin, er, Mathematical Notation?
[1] Assuming that you don't get an answer like "a monad is a monoid in the category of endofunctors," which unfortunately does tend to be the case for higher mathematical concepts.
This 'argument' always just seems to be a thinly veiled excuse to avoid putting in the bare minimum effort required to understand a complicated topic.
An opinion that’s largely held by programmers and not people who actually do maths. You learn the symbols and notation as you go and it very quickly becomes understandable. I certainly Duns I have less issues understanding mathematical notation than I do reading some programming languages.
> how is one supposed to search for ℜ? That’s chalkboard R, represents the real numbers. Searching “fancy R mathematics” (in Duck duck go) nets a page that explains what the chalkboard R, N, P, Q and C symbols all mean.
> Is it really too much to be ask to be taught in vernacular English Mathematical texts used to be written in plain English without the notation, it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
The "people who actually do maths" will almost by definition exclude anyone who has issues understanding the notation. You need to look at the latter group of people to work out if the notation is unnecessarily obtuse.
> it’s honestly so, so much worse. It’s multitude more verbose and so much harder to grasp.
As a counterexample, consider the proof that undirected Hamiltonian cycles is NP-complete, by reduction from directed Hamiltonian cycles. Karp's original paper says literally just this:
N = V × {0, 1, 2}
A = {{<u,0>, <u,1>}, {<u,1>, <u,2>} | u ∈ V} ∪ {{<u,2>,<v,0>} | <u,v> ∈ E}
By contrast, a vernacular English description would look like this:
Replace every node in the directed graph with a set of three nodes in a line. Gather all the incoming edges to the first node, and all the outgoing edges to the last node. Every path that visits every node exactly once must reach the middle node by starting at the first node and going through to the last node, and thence to the first node of a corresponding subsequent node, so every Hamiltonian path in the undirected graph is a Hamiltonian path in its directed counterpart.
More verbose, yes, but (IMO) easier to grasp.
(You can probably tell I didn't enjoy the experience...)
The article "Why 'Functor' Doesn't Matter" [0] is relevant.
In this case, the turnstile symbol comes from logic, and means "entails": Given the information on the left, you can derive the judgement on the right. There is an important distinction to be made between the turnstile and the double arrow [1].
For what it's worth, I haven't formally learned higher-level math, but I've been able to pick up type theory notation just by getting used to it. I can't necessarily explain how; it was just a gradual thing for me.
[0] https://www.parsonsmatt.org/2019/08/30/why_functor_doesnt_ma...
[1] https://math.stackexchange.com/questions/286077/implies-righ...
[1] https://www.google.com/books/edition/Advanced_Topics_in_Type...