updates to citations of SF in Lambda
This commit is contained in:
parent
f5982fd3bd
commit
e99a33fb18
2 changed files with 12 additions and 8 deletions
|
@ -4,8 +4,8 @@ layout : page
|
||||||
permalink : /Lambda/
|
permalink : /Lambda/
|
||||||
---
|
---
|
||||||
|
|
||||||
[Parts of this chapter take their text from chapter _Stlc_ in
|
[Parts of this chapter take their text from chapter _Stlc_
|
||||||
book _Programming Language Foundations_ of _Software Foundations_.
|
of _Software Foundations_ (_Programming Language Foundations_).
|
||||||
Those parts will be revised.]
|
Those parts will be revised.]
|
||||||
|
|
||||||
The _lambda-calculus_, first published by the logician Alonzo Church in
|
The _lambda-calculus_, first published by the logician Alonzo Church in
|
||||||
|
@ -35,7 +35,8 @@ variables, partly because such terms are easier to read and partly
|
||||||
because the development is more traditional.
|
because the development is more traditional.
|
||||||
|
|
||||||
The development in this chapter was inspired by the corresponding
|
The development in this chapter was inspired by the corresponding
|
||||||
development in Chapter STLC of _Software Foundations_. We differ by
|
development in Chapter _Stlc_ of _Software Foundations_
|
||||||
|
(_Programming Language Foundations_). We differ by
|
||||||
representing contexts explicitly (as lists pairing identifiers with
|
representing contexts explicitly (as lists pairing identifiers with
|
||||||
types) rather than as partial maps (which take identifiers to types),
|
types) rather than as partial maps (which take identifiers to types),
|
||||||
which will corresponds better to our subsequent development of DeBruin
|
which will corresponds better to our subsequent development of DeBruin
|
||||||
|
|
|
@ -4,18 +4,20 @@ layout : page
|
||||||
permalink : /LambdaProp/
|
permalink : /LambdaProp/
|
||||||
---
|
---
|
||||||
|
|
||||||
[Parts of this chapter take their text from chapter StlcProp in
|
[Parts of this chapter take their text from chapter _Stlc_
|
||||||
_Software Foundations: Programming Language Foundations_.
|
of _Software Foundations_ (_Programming Language Foundations_).
|
||||||
Those parts will be revised.]
|
Those parts will be revised.]
|
||||||
|
|
||||||
This chapter develops the fundamental theory of the Simply
|
This chapter develops the fundamental theory of the Simply
|
||||||
Typed Lambda Calculus, particularly progress and preservation.
|
Typed Lambda Calculus, particularly progress and preservation.
|
||||||
|
|
||||||
The development in this chapter was inspired by the corresponding
|
The development in this chapter was inspired by the corresponding
|
||||||
development in Chapter STLCProp of _Software Foundations_. It will turn
|
development in Chapter _StlcProp_ of _Software Foundations_
|
||||||
|
(_Programming Language Foundations_). It will turn
|
||||||
out that one of our technical choices in the previous chapter
|
out that one of our technical choices in the previous chapter
|
||||||
(to introduce an explicit judgment `Γ ∋ x ⦂ A`) permits a somewhat
|
(to introduce an explicit judgment `Γ ∋ x ⦂ A` in place of
|
||||||
simpler development. In particular, we can prove substitution preserves
|
treating a context as a function from identifiers to types)
|
||||||
|
permits a simpler development. In particular, we can prove substitution preserves
|
||||||
types without needing to develop a separate inductive definition of the
|
types without needing to develop a separate inductive definition of the
|
||||||
`appears_free_in` relation.
|
`appears_free_in` relation.
|
||||||
|
|
||||||
|
@ -780,6 +782,7 @@ false, give a counterexample.
|
||||||
|
|
||||||
|
|
||||||
#### Exercise: 2 stars, optional (stlc_variation6)
|
#### Exercise: 2 stars, optional (stlc_variation6)
|
||||||
|
|
||||||
Suppose instead that we add the following new rule to the typing
|
Suppose instead that we add the following new rule to the typing
|
||||||
relation:
|
relation:
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue