다믜

프로그래밍과 증명을 합니다.
I write programs and proofs. Type theory, Separation logic, Haskell, Agda, Rocq, Nix.

[다믜 @damhiya]

(한국어) 하스켈 디스코드 들어오세요
https://t.co/0eTCm5S3hJ

[다믜 @damhiya]

@gnugnubbi 수면유도제 드���시오

[다믜 @damhiya]

@typememetics Progress and preservation is a proof technique for the safety of a type system, not the definition of it. A type system can be safe without satisfying progress and preservation.

[다믜 @damhiya]

@gnugnubbi 아니 영어 철자가 다른데… Lorentz Lorenz

[다믜 @damhiya]

@gnugnubbi 로렌츠가 아니라 로렌즈 끌개임

[다믜 @damhiya]

@chabulhwi 마음이 시키는걸 하십시오

[다믜 @damhiya]

@blackenedgold 물론 trust base의 질을 단순히 코드 라인수로만 평가 할 수는 없겠지만요.

[다믜 @damhiya]

@blackenedgold https://t.co/P7Tmvcsamr
이 논문에서 조사한 바에 따르면 Rocq의 커널은 OCaml 41K줄, Lean의 커널은 C++ 8K 줄 이라고 합니다. C++ 보다는 OCaml이 더 신뢰할 수 있는 언어지만 5배 라인 수 차이가 나면 Rocq이 Lean보다 trust base의 크기 측면에서 더 낫다고 하긴 힘든것 같아요.

[다믜 @damhiya]

@blackenedgold undefined 값은 이견이 있을 수 있지만 도메인 이론 관점에서는 자연스러운것 같아요.
Rocq과 Lean은 각자 더 깔끔한 면도 있고 지저분한 면이 있는데, 개발환경 같은 공학적인 부분을 제외하면 Rocq은 subject reduction 같은 메타성질이 성립하지만 universe polymorphism은 Lean이 잘 되어 있어요.

[다믜 @damhiya]

@ridyeamnuim 와우

[다믜 @damhiya]

@ridyeamnuim 음 안되는것 같네요. 완성된 증명 타입체킹은 해볼 수 있는데, goal 보는건 emacs나 vscode 플러그인 까셔야 할듯

[다믜 @damhiya]

@dimenerno unique existence 말고 "T₁이 존재성을 보장하는 집합" 같은 개념에 대응하는게 있나요?

[다믜 @damhiya]

@dimenerno 궁금한게 있는데, 마지막 예문은 어떻게 형식화 하나요? 이런게 생각나는데...

(1) (⊢ ∃!x. ϕ(x)) → (⊢ ∀x. ϕ(x) → ∀ a b c. a ≠ b → b ≠ c → c ≠ a → ¬ (a ∈ x ∧ b ∈ x ∧ c ∈ x))

(2) (⊢ ∃!x. ϕ(x)) 이고 M이 T₁의 모델이면, ϕ(x)를 만족하는 x ∈ M 은 |x|≤2 이다.

[다믜 @damhiya]

@dimenerno 성관계 못하면 어른도 아니라는 말이군요

[joomy @ ICFP @joomy]

ok but hear me out

[다믜 @damhiya]

https://t.co/biwn9e914l

[다믜 @damhiya]

이거 대충 보고 쓴건데 같은 말이었음

[SSRS @SSRS_cp]

これは「群の演算と両立す���同値関係における単位元の同値類」が一番正しい説明だと思っている

[다믜 @damhiya]

Normal subgroup 보다 군의 연산을 보존하는 동치류
a ~ a' → b ~ b' → a·b ~ a'·b'
a ~ a' → a⁻¹ ~ a'⁻¹
e ~ e
가 자연스럽고 동기부여하기 좋다고 생각함

[다믜 @damhiya]

@kikx cubical agda를 쓰면 truncation을 정의할 수 있기 때문에 h-prop이 꽤 쓸만하지만, impredicative하게 쓰고 싶으면 propositional resizing을 따로 가정해야 합니다.

[다믜 @damhiya]

@kikx Agda는 predicative한 시스템이라 Rocq/Lean의 Prop 같은건 없어요. Predicative & definitionally proof irrelevant한 Prop은 있지만 제약이 많고, HoTT식 h-proposition은 정의할 수 있지만 cubical 모드가 아니면 propositional truncation을 정의 할 수 없어서 별 ��모가 없어요.