Γ is typically used to denote the context, or the type environment for an expression. It is a mapping from variables to types. for example we could have

Γ = x:A, y:B, z:C

then

Γ |- y: B

is a typing judgment. Means "In the context of Γ, y has type B."

Type derivation is a process where you start with an expression and an empty context and then figure out what the type of that expression is by building it up from scratch using typing rules. It's what compilers do to figure out whether your program is correct.

[–] edinbruh@feddit.it 2 points 16 hours ago

https://feddit.it/comment/20528152

[–] edinbruh@feddit.it 1 points 1 day ago (1 children)

Oooooohhh! That's my field of study!

So, you know how in programming you have data types (like int, float, structs etc...) well, they are actually math.

In math, more specifically in logics, there's these things called "judgement derivation systems". They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.

You see, one day Mr Howard wrote to Mr Curry: "I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction" and curry answered: "wow, that's cool, I'll tell you more, a type system for this other thing kinda looks like combinatory logics" and then they both went "could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?" And this is what modern type theory (and theorem provers) are based on.

Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a "context" object, which is often identified with the letter gamma.

[–] CanadaPlus 1 points 7 hours ago* (last edited 7 hours ago) (1 children)

What's the easiest way to actually learn how the correspondence works? It always feels like there's some kind of background they're assuming I have, that my pure maths ass doesn't.

[–] edinbruh@feddit.it 1 points 4 hours ago* (last edited 4 hours ago)

I'll give you a fast-forward of the subjects you need to study to actually learn this stuff (with links). Many of these are part of typical computer science curriculums. However, most will exclude at least some of this to its fullest. Note that it's a lot of knowledge, you might find it frustrating to just deep dive into it on your own, don't take it the wrong way, maybe follow an actual course and you will be guided into all of this. Maybe I'll also try to give a run-down, skipping the preupedeitic knowledge... later... if I have time.

P.s.: to get the general feeling you don't really need to know all of this tho. Just skim it. And dive deeper if you like it.

Any respectable computer scientist needs to know at least some first order logic https://en.wikipedia.org/wiki/First-order_logic
- Read the semantics part. You don't need everything, but you must understand what it means for a Formula to be a logic consequence of a set of formulas
- Read a bit the deductive systems part. I find "natural deduction" (in detail here https://en.wikipedia.org/wiki/Natural_deduction) easier to understand (more... Natural) however, your mileage may vary, many people find it confusing, hence why "sequent calculus" was invented. We'll use the sequent calculus later
You need to know lambda calculus https://en.wikipedia.org/wiki/Lambda_calculus If you know any functional programming language it will be easier, but it's optional
- You can learn it on its own, but it fits better as part of a "foundations of computer science" course. I don't have a link for that.
You also need to know a bit of programming in basically any strongly-typed language. This will give you some kind of general idea of what types and type systems are.
Now you can put together what you know of types and sequent calculus, and learn what type derivation rule are https://en.wikipedia.org/wiki/Typing_rule
- Now you understand the meme
- You can also check out what type systems are as a whole https://en.wikipedia.org/wiki/Type_system
- We have skipped Curry-Howard, but you can see how typing rules look a lot like logic deduction rules, in particular sequent calculus
Hooray, time for Curry-Howard https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence they basically notice the same similarity you just noted, but take it a step further, they can do it because they know other logics other than first order logic
The next step, if you are interested, are theorem provers, which are the direct application of the correspondence https://en.wikipedia.org/wiki/Proof_assistant
- Check out rocq or agda