Commit Graph

23 Commits (master)

Author SHA1 Message Date
James T. Martin bb53c1b162
WIP C bootstrap VM of a classical linear language. 2022-07-25 22:28:27 -07:00
James T. Martin 88e9dabddf
A few small random old things. 2022-04-18 16:14:15 -07:00
James T. Martin 65ac3994b8
It works! It works! (LEM-based assembly coroutines.) 2022-03-31 21:25:05 -07:00
James T. Martin edfa1c3c00
WIP assembly implementation of classical linear semantics. 2022-03-31 19:17:16 -07:00
James T. Martin 757e4a5f6d
Basic-ally pain and suffering. 2022-03-26 20:14:03 -07:00
James T. Martin 2b585cd1ae
Not sure. Some basic-related stuff. 2022-03-25 17:42:41 -07:00
James T. Martin 5a8eca0481
WIP basic logic cuts 2022-03-21 19:22:07 -07:00
James T. Martin 9efab5e286
Does substitution finally compute definitionally? I believe it will!
I've learned a lot about maximizing laziness and its
relation to getting shit to compute on open terms over
these last few days. I believe this lesson will remain relevant
for many years to come.

Also, deleted zipper because I'm pretty sure it can't be made
lazy even in principle, and therefore it is useless.
2022-03-18 09:53:21 -07:00
James T. Martin 36333b9537
I forgot lol 2022-03-17 08:58:10 -07:00
James T. Martin eb28c76b1b
Finally got my stupid freaking constructors to compute! 2022-03-16 14:43:46 -07:00
James T. Martin 5df3d65042
Why won't my shit compute!? (p.s. equality is the root of all evil.) 2022-03-16 12:36:17 -07:00
James T. Martin 4e3698ed84
Agonizingly tediously moving stuff to use new subst. 2022-03-15 21:04:33 -07:00
James T. Martin 9bb12148b5
Substitution, attempt 4-ish? Prev was too complicated for proofs.
(This one is quite nice! And I actually understand how it works.)
2022-03-15 15:38:52 -07:00
James T. Martin b0a3938db8
Proved unique typing, unique type derivations, & subject reduction. 2022-03-14 21:53:34 -07:00
James T. Martin bb5116e951
Typed reduction derivations (again). 2022-03-14 18:13:58 -07:00
James T. Martin 88fe4fdc8f
Typed substitution: finally correct? 2022-03-14 15:46:43 -07:00
James T. Martin 174c45ac01
Frustrating broken crap. 2022-03-14 11:54:54 -07:00
James T. Martin 6616128f73
Added typing judgements and untyped reduction. 2022-03-14 07:36:22 -07:00
James T. Martin 8ccb5f0c26
New substs which will hopefully work maybe.
It's much more general and less ad-hoc.
On the other hand, I have no idea how it works (or if it works).
I derived it pretty much by just writing out the type and putting
in whatever I hoped would make the typechecker happy.

I came up with that particular type signature by working on
the new linear derivations, which require much more sophisticated
types of substitution than I originally accounted for. I believe
substs will be sufficiently general (if it works!!).
2022-03-13 22:58:42 -07:00
James T. Martin 45ca5caec9
Linear substitution for linear terms which *hopefully* works. 2022-03-13 17:01:52 -07:00
James T. Martin 360cfec241
Partial work towards normalization (not much). 2022-03-13 12:03:00 -07:00
James T. Martin 47be20183f
Improving the formulation of derivations. 2022-03-12 19:02:13 -08:00
James T. Martin 1b85cbbd0d
Defining terms and conversions for dependent type theory. 2022-03-11 20:58:25 -08:00