810 lines
21 KiB
Plaintext
810 lines
21 KiB
Plaintext
|
|
||
|
|
Context:
|
||
|
|
|
||
|
|
[additional facts about limits on cuts
|
||
|
|
robdockins@fastmail.fm**20140818025955
|
||
|
|
Ignore-this: 6f9c952db425df6ae9d2a14139a8a3d1
|
||
|
|
]
|
||
|
|
|
||
|
|
[work on limits
|
||
|
|
robdockins@fastmail.fm**20140817221707
|
||
|
|
Ignore-this: 9811e0cd669b48f3beb7a56d47cbe3c3
|
||
|
|
]
|
||
|
|
|
||
|
|
[finish proving that Q field ops commute with injq
|
||
|
|
robdockins@fastmail.fm**20140817060600
|
||
|
|
Ignore-this: a1f6c62b39983e6f6f01d28aca5f8534
|
||
|
|
]
|
||
|
|
|
||
|
|
[split up realdom.v and perform associated code motion
|
||
|
|
robdockins@fastmail.fm**20140817030034
|
||
|
|
Ignore-this: 24c74cd459d2ab15dcd3d83ba06f7081
|
||
|
|
]
|
||
|
|
|
||
|
|
[recip is canonical and converges
|
||
|
|
robdockins@fastmail.fm**20140725211947
|
||
|
|
Ignore-this: c100dbd94114cca9576b2a3f46c9ddc7
|
||
|
|
]
|
||
|
|
|
||
|
|
[improve the proof that 1 is a unit for multiplication
|
||
|
|
robdockins@fastmail.fm**20140724150124
|
||
|
|
Ignore-this: c5ec976f8a9858a7ba1f704b4e84d02e
|
||
|
|
]
|
||
|
|
|
||
|
|
[complete proof the interval multiplication converges; other minor stuff
|
||
|
|
robdockins@fastmail.fm**20140724015132
|
||
|
|
Ignore-this: bc717baa4c8f9ec31b821c5cfae5b499
|
||
|
|
]
|
||
|
|
|
||
|
|
[further progress in realdom.v
|
||
|
|
robdockins@fastmail.fm**20140723004023
|
||
|
|
Ignore-this: f33e18d22ae69c9b6209e28151d18017
|
||
|
|
]
|
||
|
|
|
||
|
|
[unmessify rational_intervals patch
|
||
|
|
robdockins@fastmail.fm**20140721123718
|
||
|
|
Ignore-this: 4a125b192a9964a508a1063845e9f160
|
||
|
|
]
|
||
|
|
|
||
|
|
[messy updates to rational_intervals.v
|
||
|
|
robdockins@fastmail.fm**20140721015810
|
||
|
|
Ignore-this: 858dac9c55426167c6f397a71ef3fda5
|
||
|
|
]
|
||
|
|
|
||
|
|
[implicit arguments for "fixes"
|
||
|
|
robdockins@fastmail.fm**20140721015739
|
||
|
|
Ignore-this: 229ecdd48265fc855319141e399bc522
|
||
|
|
]
|
||
|
|
|
||
|
|
[metadata
|
||
|
|
robdockins@fastmail.fm**20140714201441
|
||
|
|
Ignore-this: aa16faaf09c1c404bdc6eaf0d0c39912
|
||
|
|
]
|
||
|
|
|
||
|
|
[further beautification
|
||
|
|
robdockins@fastmail.fm**20140714200516
|
||
|
|
Ignore-this: 47d74c51d9fe130a5ac12706b1ddb1d4
|
||
|
|
]
|
||
|
|
|
||
|
|
[start working on the recripricol function
|
||
|
|
robdockins@fastmail.fm**20140714180055
|
||
|
|
Ignore-this: c7f93cea17f46daa78a1ea14e86dfcaf
|
||
|
|
]
|
||
|
|
|
||
|
|
[tweaks to the lambda models
|
||
|
|
robdockins@fastmail.fm**20140714180031
|
||
|
|
Ignore-this: 219788fe70f42f0f6e60176cab464f19
|
||
|
|
]
|
||
|
|
|
||
|
|
[beauty edits in st_lam*
|
||
|
|
robdockins@fastmail.fm**20140714180006
|
||
|
|
Ignore-this: a40aa7ae00ed27595ee04073918bd028
|
||
|
|
]
|
||
|
|
|
||
|
|
[move stuff to rational_intervals.v / define real_mult and prove some properties
|
||
|
|
robdockins@fastmail.fm**20140712053232
|
||
|
|
Ignore-this: 398c5c03aac9ff37526d4d7c9e1a82c0
|
||
|
|
]
|
||
|
|
|
||
|
|
[finish correctness proof for interval multiplication
|
||
|
|
robdockins@fastmail.fm**20140711191547
|
||
|
|
Ignore-this: c9ab138a0ca43fe0b133b208419bbcc4
|
||
|
|
]
|
||
|
|
|
||
|
|
[break out facts about rational intervals
|
||
|
|
robdockins@fastmail.fm**20140711012320
|
||
|
|
Ignore-this: b7fe6e9377629a89b5debe3019ae1aa
|
||
|
|
]
|
||
|
|
|
||
|
|
[updates to ideal completion
|
||
|
|
robdockins@fastmail.fm**20140707053800
|
||
|
|
Ignore-this: 90d1efbd0e5833d8c83f0df056d7a74c
|
||
|
|
]
|
||
|
|
|
||
|
|
[a pile of additional properties in realdom.v
|
||
|
|
robdockins@fastmail.fm**20140707053519
|
||
|
|
Ignore-this: 7edba1e72a1856f297ef11e698ed989f
|
||
|
|
]
|
||
|
|
|
||
|
|
[some properties of converging prereals
|
||
|
|
robdockins@fastmail.fm**20140706041401
|
||
|
|
Ignore-this: 273bfbb245302becd7ff402831827ffb
|
||
|
|
]
|
||
|
|
|
||
|
|
[make realdom compile
|
||
|
|
robdockins@fastmail.fm**20140630015439
|
||
|
|
Ignore-this: 8bfc8eaeed4a1596450b0bb9ddef9aaa
|
||
|
|
]
|
||
|
|
|
||
|
|
[renaming
|
||
|
|
robdockins@fastmail.fm**20140630011639
|
||
|
|
Ignore-this: a287e083af095790cbf2b48df7a58739
|
||
|
|
]
|
||
|
|
|
||
|
|
[reorganize some code
|
||
|
|
robdockins@fastmail.fm**20140630011446
|
||
|
|
Ignore-this: f1375b9e7ad822cb92f0c83d4001eddd
|
||
|
|
]
|
||
|
|
|
||
|
|
[build the retract for realdom
|
||
|
|
robdockins@fastmail.fm**20140630001245
|
||
|
|
Ignore-this: 4eb9da621588417d1b7b2fc980c7bf70
|
||
|
|
]
|
||
|
|
|
||
|
|
[fill out lemmas about cPLT
|
||
|
|
robdockins@fastmail.fm**20140630001140
|
||
|
|
Ignore-this: add9e45c14621e3d6328684098bf8461
|
||
|
|
]
|
||
|
|
|
||
|
|
[more facts about cPLT
|
||
|
|
robdockins@fastmail.fm**20140628073731
|
||
|
|
Ignore-this: 101a131ed114902924a1707eff7ebc70
|
||
|
|
]
|
||
|
|
|
||
|
|
[continuous domains as retracts of bifinite domains
|
||
|
|
robdockins@fastmail.fm**20140628035522
|
||
|
|
Ignore-this: 5e7c61d49cf8424412b0d94f5fcb5ee6
|
||
|
|
]
|
||
|
|
|
||
|
|
[start implementing arithmetic operations in RealDom
|
||
|
|
robdockins@fastmail.fm**20140620003249
|
||
|
|
Ignore-this: c28479b8a933cba263765bdddb112264
|
||
|
|
]
|
||
|
|
|
||
|
|
[define the domain of rational intervals
|
||
|
|
robdockins@fastmail.fm**20140619040809
|
||
|
|
Ignore-this: 6cbe1a9cc690e5a9d77f37ee299154b
|
||
|
|
this domain is useful for describing the semantics of exact real arithmetic.
|
||
|
|
]
|
||
|
|
|
||
|
|
[show that every effective CUSL is Plotkin
|
||
|
|
robdockins@fastmail.fm**20140619034433
|
||
|
|
Ignore-this: d529a4b1d6d698f79572caa805072394
|
||
|
|
]
|
||
|
|
|
||
|
|
[fix notation for octothorpe
|
||
|
|
robdockins@fastmail.fm**20140614222130
|
||
|
|
Ignore-this: 3dc815825f11ceaf4f4f53e4668e6382
|
||
|
|
]
|
||
|
|
|
||
|
|
[fix for coq 8.4pl4
|
||
|
|
robdockins@fastmail.fm**20140614222049
|
||
|
|
Ignore-this: 9745904845aaf54e5569df982fc93d65
|
||
|
|
]
|
||
|
|
|
||
|
|
[move swelling lemma into finsets
|
||
|
|
robdockins@fastmail.fm**20140504080535
|
||
|
|
Ignore-this: ffa560e9aa4e4f8b15a55c1f9b1da72e
|
||
|
|
]
|
||
|
|
|
||
|
|
[documentation improvements and code motion
|
||
|
|
robdockins@fastmail.fm**20140504070008
|
||
|
|
Ignore-this: da7847f82403990342732a8ce226315c
|
||
|
|
]
|
||
|
|
|
||
|
|
[replace the old finprod
|
||
|
|
robdockins@fastmail.fm**20140504005534
|
||
|
|
Ignore-this: 606cf44422f68d66c8d2d90049e67b93
|
||
|
|
]
|
||
|
|
|
||
|
|
[remove the old finprod
|
||
|
|
robdockins@fastmail.fm**20140504005137
|
||
|
|
Ignore-this: 38bd54e16c87d27bbede08496c37bfba
|
||
|
|
]
|
||
|
|
|
||
|
|
[update st_lam_fix to use the new finprod
|
||
|
|
robdockins@fastmail.fm**20140504003627
|
||
|
|
Ignore-this: 95d0a66e99ccead89bdfef09a1c8c109
|
||
|
|
]
|
||
|
|
|
||
|
|
[update st_lam to use the new termmodel
|
||
|
|
robdockins@fastmail.fm**20140503230854
|
||
|
|
Ignore-this: c3d6b2155674b414c5c2e14b85b13760
|
||
|
|
]
|
||
|
|
|
||
|
|
[new version of finprod with a better term model
|
||
|
|
robdockins@fastmail.fm**20140503222035
|
||
|
|
Ignore-this: db63e3a063bdb6f2f579644c7b63bd1b
|
||
|
|
]
|
||
|
|
|
||
|
|
[a few more (hopefully final) lemmas about union
|
||
|
|
robdockins@fastmail.fm**20140422223924
|
||
|
|
Ignore-this: 7b95c75abef9b0d45863b5e33d1c5a37
|
||
|
|
]
|
||
|
|
|
||
|
|
[finish proofs about union
|
||
|
|
robdockins@fastmail.fm**20140422065034
|
||
|
|
Ignore-this: 2929c3cdb013c028a48022b0293b2f18
|
||
|
|
]
|
||
|
|
|
||
|
|
[powerdomain progress
|
||
|
|
robdockins@fastmail.fm**20140421064325
|
||
|
|
Ignore-this: 592f9c6046f05a27897b460edb2efe10
|
||
|
|
Show that powerdomains are endofunctors on PLT. Further, they are monads with
|
||
|
|
the 'singleton' and 'join' operations. Also make some progress on the additive
|
||
|
|
portion of the theory, dealing with emptyset and union.
|
||
|
|
]
|
||
|
|
|
||
|
|
[tweak makefile
|
||
|
|
robdockins@fastmail.fm**20140420031337
|
||
|
|
Ignore-this: d5954b26f731bfed3d79cefacab322fb
|
||
|
|
]
|
||
|
|
|
||
|
|
[show that semvalue is the weakest condition allowing beta-reduction of strict functions
|
||
|
|
robdockins@fastmail.fm**20140420020447
|
||
|
|
Ignore-this: 16a7ed23f04879f1fb324bdac8a2ffaf
|
||
|
|
]
|
||
|
|
|
||
|
|
[some additional operations relating to the PLT adjunction
|
||
|
|
robdockins@fastmail.fm**20140420020351
|
||
|
|
Ignore-this: db8eec6e3f74cce3acb67d2b660b104e
|
||
|
|
]
|
||
|
|
|
||
|
|
[finish building power domain fmap
|
||
|
|
robdockins@fastmail.fm**20140420020217
|
||
|
|
Ignore-this: 556e1cb87576de36cb26f8add3a1b163
|
||
|
|
]
|
||
|
|
|
||
|
|
[fix up st_lam.v
|
||
|
|
robdockins@fastmail.fm**20140329015058
|
||
|
|
Ignore-this: 1c31d674b759fbd0cc74fb3125579f96
|
||
|
|
]
|
||
|
|
|
||
|
|
[push some proofs into finprod
|
||
|
|
robdockins@fastmail.fm**20140329000401
|
||
|
|
Ignore-this: 49070fdd951e49473e60d3cd0ec431c6
|
||
|
|
]
|
||
|
|
|
||
|
|
[documentation and aesthetic changeds
|
||
|
|
robdockins@fastmail.fm**20140327043141
|
||
|
|
Ignore-this: be27b24b78ea6af722a307117e59f5b3
|
||
|
|
]
|
||
|
|
|
||
|
|
[finish the st_lam_fix example
|
||
|
|
robdockins@fastmail.fm**20140322011153
|
||
|
|
Ignore-this: e702f564b6eab2f8c11ab16bcb62504b
|
||
|
|
]
|
||
|
|
|
||
|
|
[clarafications re: countable choice; remove unfinished example from build order
|
||
|
|
robdockins@fastmail.fm**20140321212852
|
||
|
|
Ignore-this: 2a9d5c79c05ba088e1815feab99a5f6c
|
||
|
|
]
|
||
|
|
|
||
|
|
[break the "fixes" operator into a separate file and prove some facts about it
|
||
|
|
robdockins@fastmail.fm**20140318013247
|
||
|
|
Ignore-this: 80c506cef0719a974a049a1f5870f676
|
||
|
|
]
|
||
|
|
|
||
|
|
[minor fix to skiy.v
|
||
|
|
robdockins@fastmail.fm**20140317054057
|
||
|
|
Ignore-this: ffef6fcaf5fa7f8cea80d2808caf4f4c
|
||
|
|
]
|
||
|
|
|
||
|
|
[add the fixpoint operator; admit proofs
|
||
|
|
robdockins@fastmail.fm**20140317044648
|
||
|
|
Ignore-this: 97ca18e980cdf46a9b40c8252badef14
|
||
|
|
]
|
||
|
|
|
||
|
|
[remove the evaluation case for variables
|
||
|
|
robdockins@fastmail.fm**20140317032932
|
||
|
|
Ignore-this: e46d634e735e5b21a18518a48777168d
|
||
|
|
]
|
||
|
|
|
||
|
|
[start on STLC with fixpoints -- but without fixpoints for now
|
||
|
|
robdockins@fastmail.fm**20140317031953
|
||
|
|
Ignore-this: 3458bc18c73d967bef58418bc73e06cb
|
||
|
|
]
|
||
|
|
|
||
|
|
[add the eliminator for booleans to st_lam; other additional utility lemmas
|
||
|
|
robdockins@fastmail.fm**20140317031753
|
||
|
|
Ignore-this: 369dd375755cbd9ae5e3c969f3ef6ec
|
||
|
|
]
|
||
|
|
|
||
|
|
[some minor code motion
|
||
|
|
robdockins@fastmail.fm**20140228064927
|
||
|
|
Ignore-this: 804828472ddb0c5fafc72460fce8387b
|
||
|
|
]
|
||
|
|
|
||
|
|
[plug final holes in st_lam and add to build order
|
||
|
|
robdockins@fastmail.fm**20140228044729
|
||
|
|
Ignore-this: 3edc7f36bfa97775ba33ffa27c80df59
|
||
|
|
]
|
||
|
|
|
||
|
|
[reduce st_lam.v to facts I believe about fresh variables
|
||
|
|
robdockins@fastmail.fm**20140228010832
|
||
|
|
Ignore-this: bde3e73291ddd32337d6fb999e4b1c02
|
||
|
|
]
|
||
|
|
|
||
|
|
[fix breakages
|
||
|
|
robdockins@fastmail.fm**20140226073930
|
||
|
|
Ignore-this: 9be54f5255f8ed9d53a79260e9bdf565
|
||
|
|
]
|
||
|
|
|
||
|
|
[more work on lambdas
|
||
|
|
robdockins@fastmail.fm**20140226043753
|
||
|
|
Ignore-this: 7f7452670221e2643067a3c7cc180998
|
||
|
|
]
|
||
|
|
|
||
|
|
[use new finprod implementation
|
||
|
|
robdockins@fastmail.fm**20140226043700
|
||
|
|
Ignore-this: c9e05df5fcfd31254ed7318fe693490c
|
||
|
|
]
|
||
|
|
|
||
|
|
[remove old finprod
|
||
|
|
robdockins@fastmail.fm**20140226043642
|
||
|
|
Ignore-this: 2705703a2c782da21a152fbb27c8a972
|
||
|
|
]
|
||
|
|
|
||
|
|
[rearrange the interfact to finprod
|
||
|
|
robdockins@fastmail.fm**20140226043541
|
||
|
|
Ignore-this: c44d7c478948f42b188eb8d06469abbf
|
||
|
|
]
|
||
|
|
|
||
|
|
[fill remaining holes in finprod2
|
||
|
|
robdockins@fastmail.fm**20140225205242
|
||
|
|
Ignore-this: 1eeb9b8beef92790c28918292f2a9cf4
|
||
|
|
]
|
||
|
|
|
||
|
|
[rework some stuff dealing with semidecidable predicates
|
||
|
|
robdockins@fastmail.fm**20140225092149
|
||
|
|
Ignore-this: 32b5ccb2927e08979ea92b9ef67c40f4
|
||
|
|
]
|
||
|
|
|
||
|
|
[lots of work on alpha-congrunce in lambdas
|
||
|
|
robdockins@fastmail.fm**20140225035601
|
||
|
|
Ignore-this: fbbec9dac4cb328ff4e0b25df646e0c7
|
||
|
|
]
|
||
|
|
|
||
|
|
[terminate is universal in PLT
|
||
|
|
robdockins@fastmail.fm**20140225035538
|
||
|
|
Ignore-this: abc6cd1a60578c435bf9ca596d8d0922
|
||
|
|
]
|
||
|
|
|
||
|
|
[new attack on nominal finite products
|
||
|
|
robdockins@fastmail.fm**20140225035516
|
||
|
|
Ignore-this: 3875e713acc6aa5193696612f3ede76d
|
||
|
|
]
|
||
|
|
|
||
|
|
[push forward a little on lambdas
|
||
|
|
robdockins@fastmail.fm**20140221095249
|
||
|
|
Ignore-this: c690a1b03075702e3fd84aac7e268211
|
||
|
|
]
|
||
|
|
|
||
|
|
[update finprod for various changes
|
||
|
|
robdockins@fastmail.fm**20140221095230
|
||
|
|
Ignore-this: a6d787930ed356ae2b0a003af1f4d44
|
||
|
|
]
|
||
|
|
|
||
|
|
[better discrete cases lemma
|
||
|
|
robdockins@fastmail.fm**20140219051301
|
||
|
|
Ignore-this: f0ec88e8207257e7657ced933cf687e7
|
||
|
|
]
|
||
|
|
|
||
|
|
[start working on simply-typed lambdas
|
||
|
|
robdockins@fastmail.fm**20140219051238
|
||
|
|
Ignore-this: 69bea345376ea39cd1addc0849a43077
|
||
|
|
]
|
||
|
|
|
||
|
|
[more messing about with advanced category theory stuff
|
||
|
|
robdockins@fastmail.fm**20140211095003
|
||
|
|
Ignore-this: 9cd3c9d961349e8797f109f716c5f678
|
||
|
|
]
|
||
|
|
|
||
|
|
[minor rearrangements and code motion
|
||
|
|
robdockins@fastmail.fm**20140211041724
|
||
|
|
Ignore-this: 642ad6f1395fde7ecd81e5a905fd5428
|
||
|
|
]
|
||
|
|
|
||
|
|
[some basic bicategory theory
|
||
|
|
robdockins@fastmail.fm**20140210083634
|
||
|
|
Ignore-this: f47a898fa045a397d3ee70e1512b8baa
|
||
|
|
]
|
||
|
|
|
||
|
|
[even more notation futzing
|
||
|
|
robdockins@fastmail.fm**20140209072416
|
||
|
|
Ignore-this: d2061652cb3e80f6994f567a9e677b32
|
||
|
|
]
|
||
|
|
|
||
|
|
[additional notational futzing
|
||
|
|
robdockins@fastmail.fm**20140209043308
|
||
|
|
Ignore-this: ac42cbbc94df227e6d5e70b96ae65fd3
|
||
|
|
]
|
||
|
|
|
||
|
|
[futz around with notations, various other cleanup activities
|
||
|
|
robdockins@fastmail.fm**20140209005551
|
||
|
|
Ignore-this: 3f41a52650aadd956ac490b62e59c1c3
|
||
|
|
]
|
||
|
|
|
||
|
|
[complete adequacy for SKI+Y
|
||
|
|
robdockins@fastmail.fm**20140206050414
|
||
|
|
Ignore-this: f730587ac7a42f3e35740976a1439f2e
|
||
|
|
]
|
||
|
|
|
||
|
|
[minor changes in cpo
|
||
|
|
robdockins@fastmail.fm**20140206014745
|
||
|
|
Ignore-this: 95244704faf1e6c336d62dc7912f9022
|
||
|
|
]
|
||
|
|
|
||
|
|
[push through most of SKI+Y adequacy
|
||
|
|
robdockins@fastmail.fm**20140205214805
|
||
|
|
Ignore-this: dc998ef45f2e919e9373bfa21a5ef8c7
|
||
|
|
]
|
||
|
|
|
||
|
|
[major simplification of the adequacy proof for SKI
|
||
|
|
robdockins@fastmail.fm**20140205185605
|
||
|
|
Ignore-this: f1f0dc46274db05f3393038dfe2775e2
|
||
|
|
]
|
||
|
|
|
||
|
|
[push forward on SKI+Y
|
||
|
|
robdockins@fastmail.fm**20140205044216
|
||
|
|
Ignore-this: daf255aa940b42c1c68ba947a356370d
|
||
|
|
]
|
||
|
|
|
||
|
|
[continue futzing with the LR statement
|
||
|
|
robdockins@fastmail.fm**20140203055601
|
||
|
|
Ignore-this: f5ef9f06d3b1a11d76317b52cec691ab
|
||
|
|
]
|
||
|
|
|
||
|
|
[start pushing on adequacy for SKI+Y
|
||
|
|
robdockins@fastmail.fm**20140202085948
|
||
|
|
Ignore-this: 956844809340fad0c13c19e9fa729b5c
|
||
|
|
]
|
||
|
|
|
||
|
|
[mostly finish soundness for SKI+Y
|
||
|
|
robdockins@fastmail.fm**20140202060633
|
||
|
|
Ignore-this: 4c75fd9eeefa1d6dad6866662abea0fd
|
||
|
|
]
|
||
|
|
|
||
|
|
[start working on a CCL example
|
||
|
|
robdockins@fastmail.fm**20140202020748
|
||
|
|
Ignore-this: 44c5d7854cc19b0f90414c2be6b3df68
|
||
|
|
]
|
||
|
|
|
||
|
|
[make id(A) a parsing-only notation
|
||
|
|
robdockins@fastmail.fm**20140202020724
|
||
|
|
Ignore-this: 68f51f754c0b89e2e815da47b901e4b1
|
||
|
|
]
|
||
|
|
|
||
|
|
[the PLT adjunction is strong monodial
|
||
|
|
robdockins@fastmail.fm**20140202020637
|
||
|
|
Ignore-this: 7b29b9a6a5e8efa07440c528ec12d7bd
|
||
|
|
]
|
||
|
|
|
||
|
|
[fix my broken version of lfp and fixup proofs
|
||
|
|
robdockins@fastmail.fm**20140202020615
|
||
|
|
Ignore-this: 3ac283481318622cbf38378e815a4f09
|
||
|
|
]
|
||
|
|
|
||
|
|
[more work on SKI + Y
|
||
|
|
robdockins@fastmail.fm**20140202020516
|
||
|
|
Ignore-this: d1f63e2ef610c6f93d03806c5426cfa5
|
||
|
|
]
|
||
|
|
|
||
|
|
[start work on SKI + Y
|
||
|
|
robdockins@fastmail.fm**20140201085039
|
||
|
|
Ignore-this: fb7a405830cf90526cddd8ce37f4da40
|
||
|
|
]
|
||
|
|
|
||
|
|
[doc corrections
|
||
|
|
robdockins@fastmail.fm**20140130015908
|
||
|
|
Ignore-this: bca4c04267bfdac8cb202651a0960d92
|
||
|
|
]
|
||
|
|
|
||
|
|
[lots of additional inline documentation
|
||
|
|
robdockins@fastmail.fm**20140129234834
|
||
|
|
Ignore-this: ab2c59add5514f44a898de1f0eece98b
|
||
|
|
]
|
||
|
|
|
||
|
|
[powerdomains form continuous functors in EMBED
|
||
|
|
robdockins@fastmail.fm**20140126234115
|
||
|
|
Ignore-this: d2ee08902f0bdb52efd7f7ce2c594469
|
||
|
|
]
|
||
|
|
|
||
|
|
[complete the powerdomain constructions; build some operations
|
||
|
|
robdockins@fastmail.fm**20140125225202
|
||
|
|
Ignore-this: 9c8f2632df05e84fc3794a338ff8720d
|
||
|
|
]
|
||
|
|
|
||
|
|
[construct the basic powerdomains--still some holes left
|
||
|
|
robdockins@fastmail.fm**20140125064541
|
||
|
|
Ignore-this: c3206d2e1e925096b3e9ff49afacef2f
|
||
|
|
]
|
||
|
|
|
||
|
|
[generalize the lfp construction to a generic chain_sup operation
|
||
|
|
robdockins@fastmail.fm**20140124183103
|
||
|
|
Ignore-this: 4cc2c1011b9f79365dcb7c76784fbfa6
|
||
|
|
]
|
||
|
|
|
||
|
|
[update makefile
|
||
|
|
robdockins@fastmail.fm**20140124073734
|
||
|
|
Ignore-this: a0b7db8383262caa314c21b99e146222
|
||
|
|
]
|
||
|
|
|
||
|
|
[new file for recursive lambda domains
|
||
|
|
robdockins@fastmail.fm**20140124070023
|
||
|
|
Ignore-this: 300c02b4da83b6ebd734aa2ccb21cd2d
|
||
|
|
]
|
||
|
|
|
||
|
|
[more lemmas about antistrict homs
|
||
|
|
robdockins@fastmail.fm**20140124065953
|
||
|
|
Ignore-this: 483c7b350dc3cab59c8ff50e1ac73b8c
|
||
|
|
]
|
||
|
|
|
||
|
|
[fix breakage related to implicit arguments
|
||
|
|
robdockins@fastmail.fm**20140124065805
|
||
|
|
Ignore-this: 561693d3280851299c6a49a2a34546b3
|
||
|
|
]
|
||
|
|
|
||
|
|
[notation tweaks in cpo.v
|
||
|
|
robdockins@fastmail.fm**20140124053800
|
||
|
|
Ignore-this: 83e92d8c14568448074a940ceafbe2c9
|
||
|
|
]
|
||
|
|
|
||
|
|
[add if/then/else to the SKI system
|
||
|
|
robdockins@fastmail.fm**20140124023630
|
||
|
|
Ignore-this: 37a9737932a05393a6338380226ca346
|
||
|
|
]
|
||
|
|
|
||
|
|
[case analysis for finite types
|
||
|
|
robdockins@fastmail.fm**20140124012505
|
||
|
|
Ignore-this: 6ec1076b2a74f5832501a105a28a6dba
|
||
|
|
]
|
||
|
|
|
||
|
|
[finish adequacy proof for SKI
|
||
|
|
robdockins@fastmail.fm**20140123211322
|
||
|
|
Ignore-this: 1fe3e626e33431c27e2aa186b3bf91d2
|
||
|
|
]
|
||
|
|
|
||
|
|
[additional lemmas about domains
|
||
|
|
robdockins@fastmail.fm**20140123090037
|
||
|
|
Ignore-this: fcad2dd816f805b8b5e7d1be3df60db8
|
||
|
|
]
|
||
|
|
|
||
|
|
[most of a proof of adequacy for SKI
|
||
|
|
robdockins@fastmail.fm**20140123085839
|
||
|
|
Ignore-this: d1595c02a6387297018e7f316a3e751
|
||
|
|
]
|
||
|
|
|
||
|
|
[more work on finite products
|
||
|
|
robdockins@fastmail.fm**20140121061158
|
||
|
|
Ignore-this: c2f8212e041478104dd4c81c225b42d5
|
||
|
|
]
|
||
|
|
|
||
|
|
[begin work on a more flexible "finprod" domain
|
||
|
|
robdockins@fastmail.fm**20140119021653
|
||
|
|
Ignore-this: 249718a2c31964733171b21c84d2effb
|
||
|
|
]
|
||
|
|
|
||
|
|
[mess with implicit arguments in categories.v
|
||
|
|
robdockins@fastmail.fm**20140113041450
|
||
|
|
Ignore-this: 314cad9207f706e949bd686aaa5c5e1b
|
||
|
|
]
|
||
|
|
|
||
|
|
[products for CPO, uniformity of lfp
|
||
|
|
robdockins@fastmail.fm**20140113041421
|
||
|
|
Ignore-this: e533abe995e634c732a35e71d66ddb6a
|
||
|
|
]
|
||
|
|
|
||
|
|
[define the LFP in pointed CPOs, prove the Scott induction principle
|
||
|
|
robdockins@fastmail.fm**20140112231843
|
||
|
|
Ignore-this: 2014174b1c6914bef376d614f34d073f
|
||
|
|
]
|
||
|
|
|
||
|
|
[build the forgetful functor from EMBED to PLT
|
||
|
|
robdockins@fastmail.fm**20140110014909
|
||
|
|
Ignore-this: 1dacbfc0383e48f4ab35fe0a5fd11cec
|
||
|
|
]
|
||
|
|
|
||
|
|
[notation changes, prove sum_cases and curry preserve order and equality
|
||
|
|
robdockins@fastmail.fm**20140110014820
|
||
|
|
Ignore-this: d1c6a1d0346a9eba14f3529ac30b5e2f
|
||
|
|
]
|
||
|
|
|
||
|
|
[prove addl facts about pairs, tweak implicit arguments
|
||
|
|
robdockins@fastmail.fm**20140110010319
|
||
|
|
Ignore-this: 9f0af8abc268b2b22d8b5450d6a4136
|
||
|
|
]
|
||
|
|
|
||
|
|
[make 'ob' a coercion
|
||
|
|
robdockins@fastmail.fm**20140110010204
|
||
|
|
Ignore-this: 467c0b0a8b086a7f44bf98875a4380d6
|
||
|
|
]
|
||
|
|
|
||
|
|
[copyright notices
|
||
|
|
robdockins@fastmail.fm**20140106232333
|
||
|
|
Ignore-this: f59bafa0ec99e259bd9b4319f2cdbc67
|
||
|
|
]
|
||
|
|
|
||
|
|
[add ord_dec coercion
|
||
|
|
robdockins@fastmail.fm**20140104052750
|
||
|
|
Ignore-this: 4ed1cacfd27979f0fe518862be5ac27c
|
||
|
|
]
|
||
|
|
|
||
|
|
[define the model for CBV lambda calculus
|
||
|
|
robdockins@fastmail.fm**20140104050626
|
||
|
|
Ignore-this: 88ca796d4697bfebb044d3fae27d6129
|
||
|
|
]
|
||
|
|
|
||
|
|
[proof a fixpoint lemma for unpointed domains
|
||
|
|
robdockins@fastmail.fm**20140103231818
|
||
|
|
Ignore-this: 4939eb02d09b6a4eecf145c887c64393
|
||
|
|
]
|
||
|
|
|
||
|
|
[prove that the adjoint functors between PLT and PPLT extend to continuous functors in EMBED
|
||
|
|
robdockins@fastmail.fm**20140103000915
|
||
|
|
Ignore-this: 54da0101f581731ebe512ed514e0603e
|
||
|
|
]
|
||
|
|
|
||
|
|
[notation changes for PLT
|
||
|
|
robdockins@fastmail.fm**20140102234446
|
||
|
|
Ignore-this: ad1f82f22d1bf0e057f11c3508a81716
|
||
|
|
]
|
||
|
|
|
||
|
|
[move embeddings into their own file; pull TPLT and PPLT into profinite.v
|
||
|
|
robdockins@fastmail.fm**20140102234424
|
||
|
|
Ignore-this: 3704996af47ae32415ba3e539d67cf5c
|
||
|
|
]
|
||
|
|
|
||
|
|
[Show that PLT is cocartesian; rearrange proof that EMBED(true) is terminated
|
||
|
|
robdockins@fastmail.fm**20140102213805
|
||
|
|
Ignore-this: 3470df6910e7a3e4bda478c0c6ecea62
|
||
|
|
]
|
||
|
|
|
||
|
|
[remove unnecessary "inh" hypothesis in the definition of Plotkin order; fixup the fallout
|
||
|
|
robdockins@fastmail.fm**20140102213646
|
||
|
|
Ignore-this: b6a5ad59296f938b377d71852120d48b
|
||
|
|
]
|
||
|
|
|
||
|
|
[move proofs that empty and unit preorders are effective plotkin
|
||
|
|
robdockins@fastmail.fm**20140102205530
|
||
|
|
Ignore-this: 7324843510fd938d356aa82003c9ec68
|
||
|
|
]
|
||
|
|
|
||
|
|
[make epi/mono/iso morphisms into categories
|
||
|
|
robdockins@fastmail.fm**20131228082442
|
||
|
|
Ignore-this: ee75a2b6eb1f3d6fa47f17d6734e5015
|
||
|
|
]
|
||
|
|
|
||
|
|
[define the cocartesian and distributive categories
|
||
|
|
robdockins@fastmail.fm**20131226001612
|
||
|
|
Ignore-this: 11e9d8a88bef42bcb800b31d85d28d16
|
||
|
|
]
|
||
|
|
|
||
|
|
[remove uses of maximally implict arguments
|
||
|
|
robdockins@fastmail.fm**20131226001536
|
||
|
|
Ignore-this: c0d93a5398aea58cbcc4fbbca3b59b17
|
||
|
|
]
|
||
|
|
|
||
|
|
[fixpoints and binary sums for NOMINAL
|
||
|
|
robdockins@fastmail.fm**20131121092931
|
||
|
|
Ignore-this: 8a660dfe2ab16a8208ae559dcf2b7ed0
|
||
|
|
]
|
||
|
|
|
||
|
|
[modify bilimit.v to use the general construction from cont_functors.v
|
||
|
|
robdockins@fastmail.fm**20131120075848
|
||
|
|
Ignore-this: 17ea36107ade1646eab5c99aec3561a9
|
||
|
|
]
|
||
|
|
|
||
|
|
[generic fixpoint construction for categories with initial objects and directed colimits
|
||
|
|
robdockins@fastmail.fm**20131119092522
|
||
|
|
Ignore-this: 25674dff855a1cecdb4ee919f8bf3a5d
|
||
|
|
]
|
||
|
|
|
||
|
|
[remove some irritating unit parameters, fix doc typos
|
||
|
|
robdockins@fastmail.fm**20131118093204
|
||
|
|
Ignore-this: 38342d58567d8a13471620d5b7c2b7d4
|
||
|
|
]
|
||
|
|
|
||
|
|
[improvements to categories; complete some constructions in nominal
|
||
|
|
robdockins@fastmail.fm**20131118085737
|
||
|
|
Ignore-this: e58cb49a01d0210dabdb021250910adb
|
||
|
|
]
|
||
|
|
|
||
|
|
[build fixes
|
||
|
|
robdockins@fastmail.fm**20131113004305
|
||
|
|
Ignore-this: 5abffcd1d6b44f816749c5e0cfd5b6e9
|
||
|
|
]
|
||
|
|
|
||
|
|
[Documentation additions
|
||
|
|
robdockins@fastmail.fm**20131113004254
|
||
|
|
Ignore-this: 79a913d3a8652866f3fdc64891f6304d
|
||
|
|
]
|
||
|
|
|
||
|
|
[lots of inline documentation additions
|
||
|
|
robdockins@fastmail.fm**20131112192736
|
||
|
|
Ignore-this: 6aa38112c10ceed3bf43e35dbda98312
|
||
|
|
]
|
||
|
|
|
||
|
|
[update makefiles
|
||
|
|
robdockins@fastmail.fm**20131112192706
|
||
|
|
Ignore-this: d834beaa532cdf994cfa0a0b5a562e4f
|
||
|
|
]
|
||
|
|
|
||
|
|
[continuous functors for binary sum and products
|
||
|
|
robdockins@fastmail.fm**20131112192605
|
||
|
|
Ignore-this: 61520e6e315df909465a02f854816366
|
||
|
|
]
|
||
|
|
|
||
|
|
[add the category of nominal types
|
||
|
|
robdockins@fastmail.fm**20131112192520
|
||
|
|
Ignore-this: f0351c5eb0bdacdfe192a6863d9c0bc6
|
||
|
|
]
|
||
|
|
|
||
|
|
[split the proof that expF is a continuous functor into a separate file; rearrange some defintions
|
||
|
|
robdockins@fastmail.fm**20130924013328
|
||
|
|
Ignore-this: 4eacee37bb6474d1bdfffe416b98b4c1
|
||
|
|
]
|
||
|
|
|
||
|
|
[rearrange definitions of continuous functors. Prove enough plumbing to build the model: D = D->D
|
||
|
|
robdockins@fastmail.fm**20130924002837
|
||
|
|
Ignore-this: a66f9e8833601e244048b70e8bfaab96
|
||
|
|
]
|
||
|
|
|
||
|
|
[show that the function space is a continuous functor; other junk
|
||
|
|
robdockins@fastmail.fm**20130923060521
|
||
|
|
Ignore-this: d8f406450688c633ebc1fe1eb0343c91
|
||
|
|
]
|
||
|
|
|
||
|
|
[some name changes, other cosmetic fixes
|
||
|
|
robdockins@fastmail.fm**20130909043234
|
||
|
|
Ignore-this: cdd24d1c96a34fb3573c1806153df9fb
|
||
|
|
]
|
||
|
|
|
||
|
|
[additional cosmetic changes and rearrangements
|
||
|
|
robdockins@fastmail.fm**20130909020137
|
||
|
|
Ignore-this: 77d28bc9452f6c93915194033118dab7
|
||
|
|
]
|
||
|
|
|
||
|
|
[reorganize profinite code
|
||
|
|
robdockins@fastmail.fm**20130909011437
|
||
|
|
Ignore-this: 8511bf92ca6998ff8c69d5537624bdb8
|
||
|
|
]
|
||
|
|
|
||
|
|
[cosmetic changes
|
||
|
|
robdockins@fastmail.fm**20130908183909
|
||
|
|
Ignore-this: e19039701e58fd26ca4eab79d7b49d14
|
||
|
|
]
|
||
|
|
|
||
|
|
[complete the bilimit construction, show how to take fixpoints of continuous functors
|
||
|
|
robdockins@fastmail.fm**20130908175228
|
||
|
|
Ignore-this: 82feab8fdc0c944f13d91605c6a8e571
|
||
|
|
]
|
||
|
|
|
||
|
|
[find a MUCH easier path to a bilimit construction
|
||
|
|
robdockins@fastmail.fm**20130907012151
|
||
|
|
Ignore-this: fcc72ad140b045ef37e4b03ad38a8fb0
|
||
|
|
]
|
||
|
|
|
||
|
|
[lots of progress, mostly on defining bilimits
|
||
|
|
robdockins@fastmail.fm**20130905204959
|
||
|
|
Ignore-this: abf4bcf03a49fa009f9fb2200ee3abf2
|
||
|
|
]
|
||
|
|
|
||
|
|
[start working on the theory of finite preorders, which form a basis for plokin orders
|
||
|
|
robdockins@fastmail.fm**20130812054451
|
||
|
|
Ignore-this: 5be36257a8fdf486bcc31f587d93c457
|
||
|
|
]
|
||
|
|
|
||
|
|
[parameterize plotkin orders, build category PPLT
|
||
|
|
robdockins@fastmail.fm**20130811063623
|
||
|
|
Ignore-this: 3f273841bc72098acee0fd618627dbd5
|
||
|
|
]
|
||
|
|
|
||
|
|
[complete the details showing PLT is cartesian closed
|
||
|
|
robdockins@fastmail.fm**20130809230336
|
||
|
|
Ignore-this: 13fd1b5a8172dd263cf655421f7584f7
|
||
|
|
]
|
||
|
|
|
||
|
|
[add files missed in the first import
|
||
|
|
robdockins@fastmail.fm**20130809080742
|
||
|
|
Ignore-this: 6b59cce866a486d70559f7c80fe99053
|
||
|
|
]
|
||
|
|
|
||
|
|
[initial import of development
|
||
|
|
robdockins@fastmail.fm**20130809080409
|
||
|
|
Ignore-this: 44cb5a0df2f1643d289f07dcd4227cbf
|
||
|
|
First major steps toward a fully effective and usable formalized
|
||
|
|
domain theory. We formalize the plotkin preorders and show that
|
||
|
|
they form a cartesian closed category.
|
||
|
|
]
|