search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

"Gamma" in STLC #160

Open AdamBJ opened 9 years ago

AdamBJ commented 9 years ago

Can someone help me better understand the concept of gamma as it applies to STLC? Here is what I understand: gamma is related to type, and somehow maps each of the variables in a term to a type which allows us to determine the overall type of the term. I'm a bit confused about the specifics of how it accomplishes this though. Also, I don't understand some of the auxiliary functions related to gamma such as extend and extend_neq. What do these functions do and how are they related to the gamma of a term?

Thanks

justlaugh05 commented 9 years ago

Think of states in the previous chapters. extend would be like update. empty Gamma would be empty_state. Instead of holding values of variables, it holds the Types