# Penn CIS 500 - CIS 500 LECTURE NOTES (35 pages)

Previewing pages 1, 2, 16, 17, 18, 34, 35 of 35 page document
View Full Document

# CIS 500 LECTURE NOTES

Previewing pages 1, 2, 16, 17, 18, 34, 35 of actual document.

View Full Document
View Full Document

## CIS 500 LECTURE NOTES

43 views

Pages:
35
School:
University of Pennsylvania
Course:
Cis 500 - Software Foundations.
##### Software Foundations. Documents
• 34 pages

• 28 pages

• 54 pages

• 27 pages

• 8 pages

• 11 pages

• 44 pages

• 9 pages

• 6 pages

• 55 pages

• 20 pages

• 15 pages

• 35 pages

• 75 pages

• 60 pages

• 11 pages

• 16 pages

• 2 pages

• 8 pages

• 65 pages

• 63 pages

• 7 pages

• 58 pages

• 18 pages

• 28 pages

• 61 pages

• 8 pages

• 10 pages

• 10 pages

• 4 pages

• 2 pages

• 11 pages

• 6 pages

• 48 pages

• 58 pages

• 2 pages

• 18 pages

• 11 pages

Unformatted text preview:

CIS 500 Software Foundations Fall 2006 October 9 Review Church encoding of lists Church encoding of lists will not be on the exam Briefly though here s the intuition c4 s z s s s s z Church encoding of lists will not be on the exam Briefly though here s the intuition c4 s z s s s s z v1 v2 v3 v4 s z s v1 s v2 s v3 s v4 z Typing derivations Exercise 9 2 2 Show by drawing derivation trees that the following terms have the indicated types 1 f Bool Bool f if false then true else false Bool 2 f Bool Bool x Bool f if x then false else x Bool Bool The two typing relations Question What is the relation between these two statements 1 t T 2 t T The two typing relations Question What is the relation between these two statements 1 t T 2 t T First answer These two relations are completely different things I We are dealing with several different small programming languages each with its own typing relation between terms in that language and types in that language I For the simple language of numbers and booleans typing is a binary relation between terms and types t T I For typing is a ternary relation between contexts terms and types t T When the context is empty because the term has no free variables we often write t T to mean t T Conservative extension Second answer The typing relation for conservatively extends the one for the simple language of numbers and booleans I Write language 1 for the language of numbers and booleans and language 2 for the simply typed lambda calculus with base types Nat and Bool I The terms of language 2 include all the terms of language 1 similarly typing rules I Write t 1 T for the typing relation of language 1 I Write t 2 T for the typing relation of language 2 I Theorem Language 2 conservatively extends language 1 If t is a term of language 1 involving only booleans conditions numbers and numeric operators and T is a type of language 1 either Bool or Nat then t 1 T iff t 2 T Preservation and Weaking Permutation Substitution Review Proving progress

View Full Document

Unlocking...