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

Previewing pages*1, 2, 16, 17, 18, 34, 35*of 35 page document

**View the full content.**# CIS 500 LECTURE NOTES

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

**View the full content.**View Full Document

## CIS 500 LECTURE NOTES

0 0 43 views

- Pages:
- 35
- School:
- University of Pennsylvania
- Course:
- Cis 500 - Software Foundations.

**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