2
4

2 に答える 2

5

At a high level, the notation is simple: given that the conditions above the lines are held, the expression below the line is true.

Γ is a typing context--that is, it is a set of pairs of variables and types. These pairs map variables to types. The ⊢ just means "in the context". The colon just combines a variable with a type--it's like :: in Haskell or : in Scala or Ocaml. So something like Γ ⊢ x:σ means that "in context Γ, x has type σ". Something like Γ,x:σ means the context made up of Γ and x:σ.

Essentially, the context represents all the types the other variables have. So x:σ ∈ Γ means that x has type σ in Γ, which lets you trivially resolve that Γ ⊢ x:σ. All this is saying is that if x is bound to some type in a context, it has that type in that context.

You can think of the typing context as all the type information from the "outside". So the trivial statement in the above paragraph basically tells you that if you see an x and x already has type σ, you can infer that x has type σ. Not very interesting, but very important!

You could write this rule out as:

x:σ ∈ Γ
-------
Γ ⊢ x:σ

If only we had LaTeX :P. I guess we're not as cool as math.se or cstheory.se.

Here is a slightly more complicated example. Essentially, we want to encode how application works in the simply typed lambda calculus. It's actually very simple: given a function f of type τ → τ' and a value x of type τ then f x has type τ'. In Haskell, this would look like applying f :: Int -> Bool on x :: Int. It's pretty clear that f x :: Bool. So let's write this out.

The condition (the top bit) is that, in some context, f has a type τ → τ': Γ ⊢ f:τ → τ'. Also, in that same context, x has type τ: Γ ⊢ x:τ. Put together, we get: Γ ⊢ f:τ → τ' Γ ⊢ x:τ.

Now on to the bottom bit. Given these two types, what do we know? We know the type of the application f x but only in the same context. (This is why Γ matters.) So we get: Γ ⊢ f x:τ'.

And now, putting it all together, we have:

Γ ⊢ f:τ → τ' Γ ⊢ x:τ 
--------------------
     Γ ⊢ f x:τ'

Seeing the StackOverflow syntax highlighter struggle with that last example is amusing. I wonder which language it thinks that's in.

于 2012-07-13T08:26:28.220 に答える
3

The Γ (if anyone knows how to embed LaTeX please leave a comment or edit the comment) is a symbol for the typing context: you can view it as a map between an expression and it's type.

For example, let's take two contexts:

  • Γ0 the empty map and
  • Γ1 = Γ0, x:Int the previous one enriched with a type information saying that x has type Int. Thus, : here stands for type assignment.

Now, in the empty context (Γ0) there is no way to type the expression x + x because you don't know the type of x (it is not stored in the map). However, in the other context we have a type for x (that is Int) so we can say that x + x has type Int.

Formally, we have used a rule like this one:

  x : σ ∈ Γ
______________
 Γ ⊢ x + x: σ

Observe that : stands for :: in Haskell. And A ⊢ B is to be read as "in the context of A B holds.

PS: I had a course about Type Systems, you can find some of the materials here (and you may look at Typed_Lambda_Calculus.pdf).

于 2012-07-13T08:28:46.923 に答える