search

AtticusKuhn / parallel-algorithms

Proving the correctness and performance of certain parallel algorithms
4 stars 0 forks source link

No Categories #5

Closed AtticusKuhn closed 1 year ago

AtticusKuhn commented 1 year ago

Upon the advice of Conal Elliott, I am going to formalize binary arithmetic without using categories.

AtticusKuhn commented 1 year ago

I added a function extensionality axiom

  pfunext : {x y a b : Set} {f : x → y} {g : a → b} → ⦃ tyb : hasT y b ⦄ → ⦃ txa : hasT x a ⦄  →  ( (h : x) → (p⟦ f h ⟧) ≡ g (p⟦ h ⟧)) → p⟦ f ⟧ ≡ g

Basically, if ∀ x → ⟦ f x ⟧ ≡ g ⟦ x ⟧ , then ⟦ f ⟧ ≡ g. Hopefully this axiom is sound.

conal commented 1 year ago

Hopefully this axiom is sound.

What do you mean by "sound" for an axiom?

AtticusKuhn commented 1 year ago

What do you mean by "sound" for an axiom?

Perhaps a better word than "sound" is "correct".

conal commented 1 year ago

What do you mean by "sound" for an axiom?

Perhaps a better word than "sound" is "correct".

Okay. What do you mean by "correct" for an axiom?