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.
View Full Document

CIS 500 LECTURE NOTES



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

View the full content.
View Full Document
View Full Document

CIS 500 LECTURE NOTES

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

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view CIS 500 LECTURE NOTES and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CIS 500 LECTURE NOTES and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?