re: shop talk

Also to prove transitivity I think I need J anyway lol

re: shop talk

Oh! I don't. I even wrote down how in my blog post lmao

re: shop talk

Uh oh! The paper about decidability of convertibility (which also proves symmetry and transitivity) works with typed conversion. I do not have typed conversion. Whoopsie

re: shop talk

Me: Why did I add transitivity explicitly? I can derive this
Me: *a day of hunting later* I cannot derive this

re: shop talk

Why is it there are things I can prove in propeq land that I cannot prove in defeq land

re: shop talk

ah. It's because propeq is typed and defeq is not, and there's more structure in types than in syntax
If I had typed defeq I could appeal to canonicity for an approximative result, but I don't even have that

re: shop talk

Why do I have a Set universe and a Type₀ universe?

re: shop talk

Oh I think this is left over from my little experiment with impredicative Set

re: shop talk

adding some absolutely trivial translations. you love to see it

re: shop talk

I mean if you don't look too hard at it you wouldn't even notice what was wrong with it

re: shop talk

Proofs are so incredibly boring when you know they should hold

re: shop talk

I keep going back and forth on whether I actually can definitionally obtain match etas without adding the rules
I now suspect that I can do it in the one specific case where I actually use it

re: shop talk

Yup did it on paper, applying it to the concrete case works fine
Don't need the eta law yess

re: shop talk

I feel like I could prove transitivity of subtyping syntactically just using transitivity of convertibility

re: shop talk

I mean there's only like four cases
Conversion, universes, Pi types, foralls
Suppose there is a left and right subtyping derivations and I wanna combine them to get transitivity
If the left is universes then the right must be either universes, in which case it holds by universes lol, or it's convertibility, but the only thing a universe is convertible with is itself or something that reduces to itself, so it holds by... nvm I need transitivity to get across the reduction lol

re: shop talk

Wait I'm such a fool I---

re: shop talk

I finally fixed all my proofs to use equality reflection to reflect match eta but I took a closer look at the thing I needed to eta on and it was one of MY definitions
I could literally change that definition to move the match in and it would semantically (well. observationally) be the same while no longer needing match eta in the proof
I've had this in front of me for HOW many months?? and I never once questioned why exactly I really needed match eta??? I cannot believe I've caused myself all this trouble

re: shop talk

at this point literally the only reason I need equality reflection is to show that accessibility is a (weak) proposition...

re: shop talk

I'm not doing this tonight. I'm gonna fix the def and then the proof tmrw and then everything will be beautiful

re: shop talk

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

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

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

lmao immediately spotting a typo

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

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

re: shop talk

maybe you get eta just from extensionality anyway

re: shop talk

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

re: shop talk

??

re: shop talk

MetaCoq defines conversion as subtyping in both directions
hwhghwhgat

re: shop talk

the subtyping is all tangled up with the congruence rules

re: shop talk

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

re: shop talk

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

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

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

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

yeah

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

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

re: shop talk

oh it might be for inductives, like a list in universe i should be a subtype of list in universe j if i <= j
hmm... don't like that

re: shop talk

ok putting that aside, I think checking eta shouldn't need further reduction, so it can go in the ≤ judgement, but something has to take care of congruences

re: shop talk

although what's the point of defining convertibility in terms of subtyping if the typing rule uses subtyping
there's no use for convertibility anywhere anymore, except for in my proofs lol

re: shop talk

yeah it's not great for a type preservation proof since you need to show that reducing in the source and translating then reducing in the target produces convertible results...

re: shop talk

wondering for a very brief moment whether I could simply do away with function eta before remembering I actually do use it to prove function extensionality

re: shop talk

I give up. I give up! I don't know why I fell down the rabbit hole of conversion and subtyping again
There is no need for conversion to be defined in terms of subtyping, I'll leave transitivity and congruence as they are with digressions about why congruence is necessary in the presence of eta and why transitivity isn't so easily provable, and I'll forever be mystified at why subtyping itself doesn't need congruence rules

re: shop talk

----(e: poopy)(x: τ) ⊢ e x ⊳* e x----(e: poopy)(x: τ) ⊢ e x ≈ e x----(e: poopy) ⊢ λx: τ. e x ≈ e

by the same reasoning:

...----(e: poopy) ⊢ e ≈ Λα. e [α]

by transitivity, λx: τ. e x ≈ Λα. e [α]
oopsie

re: shop talk

I don't like this. I don't like this one bit. Two different head normal forms being convertible... let alone two ill-typed ones... shgjsh

re: shop talk

Anyway I'm satisfied with this resolution. Either I have no eta, explicit transitivity rule, and explicit congruence rule, or I have all of them, and that's that, no ifs ands or buts

re: shop talk

On the other hand I'm pretty sure subtyping is transitive without eta on the condition that subtyping is defined in terms of reduction and not through conversion, and proving it probably only requires confluence as usual

re: shop talk

I should probably prove confluence then huh

re: shop talk

Anyway. Transitivity doesn't hold in the source bc I have two different etas, and transitivity doesn't hold in the target because of reflection and to apply propositional transitivity I would need the type of the term on the other side which I don't have, so I need to add transitivity everywhere anyway

re: shop talk

Now that that's settled I can move on to... well idk. Whatever it was I was supposed to do next

re: shop talk

Ah yes, attend POPL

re: shop talk

Me: time to relax
Brain: don't you think untyped conversion with reflection is inconsistent
Me: shut up no it isn't

re: shop talk

⊤ ≈ let _: ⊤ ≡ ⊥ ≔ poopoopeepee in ⊤ (ζ-reduction)≈ let _: ⊤ ≡ ⊥ ≔ poopoopeepee in ⊥ (reflection)≈ ⊥ (ζ-reduction)

like there's literally no type checking to make sure you're actually giving a well-typed proof

· ⊢ ⊥: 𝒰· ⊢ tt: ⊤· ⊢ ⊤ ≈ ⊥---------· ⊢ tt: ⊥

lmao

re: shop talk

It looks like it's the combination of untyped conversion, equality reflection, transitivity, and congruence

re: shop talk

Walking up to my poster session like bad news everyone. The target language in which I've been trying to prove consistency is in fact inconsistent. Thanks for coming please help yourselves to the virtual coffee at the virtual coffee bar in your virtual mugs goodbye

re: shop talk

I mean I don't need it, but the other thing I do need hasn't been proven consistent, but at least I haven't proven it inconsistent

re: shop talk

I've figured it out
I can require typing ONLY on equality reflection, which makes sense because I should only be allowed to reflect an actual proof of equality, and this won't mess up the type preservation proof because I only go in one direction, and all of the source conversions translate to target ones WITHOUT reflecting, and where I DO actually use reflection I have, I think, sufficient typing information that nope no I don't. I do not

re: shop talk

I need a well-typed context at the very least for when I show reduction is preserving
Possibly the entire term as well

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