re: shop talk

I mean anything not covered otherwise should be covered by reduction on both sides

re: shop talk

I'm not really sure what the application/lambda/let rules are there for? Like when are those ever going to matter

re: shop talk

yeah

re: shop talk

I think on paper I can do away with e=e as I've written it down bc we can sort of implicitly understand what "syntactic equality" means without needing to write down the tedium
So I can condense this into smth smaller I think

re: shop talk

In any case it's not so obvious that subtyping is transitive this way

re: shop talk

They actually put the congruence rules inside of the 1-step ones but I personally don't like that
The 1-step reductions should be "true" reductions where substitutions occur and the other ones, reflexivity and transitivity and congruence, are just "structural" ones

re: shop talk

The reduction rules (⊳*) contain the congruent, reflexive, transitive closure of the 1-step reductions

re: shop talk

afaict THIS is the definitive version of convertibility, where syntactic equality is interrupted by subtyping

re: shop talk

the subtyping is all tangled up with the congruence rules

re: shop talk

MetaCoq defines conversion as subtyping in both directions
hwhghwhgat

re: shop talk

??

re: shop talk

eta: ∀ τ σ (e: (x: τ) → σ), λ x: τ. e x ≡ e
eta τ σ e = ?
nah there's nothing to reflect without eta

re: shop talk

maybe you get eta just from extensionality anyway

re: shop talk

I can validate my eta laws just by having them translate to a different set of eta laws right

re: shop talk

My thesis is going to have so many little details about things like this that have nothing to do with sized types lol

re: shop talk

lmao immediately spotting a typo

re: shop talk

untyped conversion... eta equivalence... cumulativity... long ago the three nations never lived in harmony actually it doesn't exist in any formal models

re: shop talk

fixed
I'm thinking about streams now. if induction on sized lists corresponds to well-founded induction on their size, what does coinduction to make streams correspond to...? it couldn't possibly be well-founded induction as well

re: shop talk

confirmed with Coq though, the guard checker says it's ok

What's the dependent types of particle physics lol

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.