[Lecture 6] Missing Assumption of Fixpoint Transfer Theorem?

[bongjunj]

이름 Your Name

장봉준

질문 Question

증명 2단계에서, $D$가 CPO라는 사실을 이용합니다.
하지만 가정 어디에도 $D$가 CPO라는 보장이 없습니다.
갈루아 연결은 $D$와 $D^\sharp$이 poset이면 되고,
연속함수도 정의역과 공역이 poset이면 됩니다.

증명 4단계에서 F의 least fixed point를 (아마도 Kleene Fixpoint Theorem을 이용해) $\bigsqcup F^i(\bot)$로 나타내는데,
Kleene Fixpoint Theorem을 이용하기 위해서도 $D$가 CPO임을 보장해야 합니다.

번역본 Translated Version

At step 2 of the proof, it uses the fact that D is a CPO.
However, there is no guarantee that D is a CPO in the assumption.
Galois connection requires $D$ and $D^\sharp$ to be posets, not CPOs.
A continuous function requests poset domain and codomains.

At step 4, the least fixed point of F is $\bigsqcup F^i(\bot)$ (probably, using Kleene Fixpoint Theorem).
The theorem requires $D$ to be a CPO too.

[KihongHeo]

Yes. Both $D$ and $D^{\sharp}$ are CPO.

[EunsuKim03]

안녕하세요, 예전에 수업끝나고 비슷한 질문을 드렸을 때, 갈루아 연결 자체가 두 CPO에 대해서 정의된다고 하셨던 것으로 기억하는데 그러면 "Let D and D# be related by Galois connection" 이라는 조건이 주어지면 별다른 언급 없이도 D와 D# 모두 CPO라고 할 수 있나요?

[KihongHeo]

그런 뜻은 아니고, 저 정리의 조건에 D, D#이 CPO 라는 조건이 들어가야 명확합니다.

The condition that D and D^# are CPOs needs to be included in the theorem to make it precise.

[bongjunj]

안녕하세요, 예전에 수업끝나고 비슷한 질문을 드렸을 때, 갈루아 연결 자체가 두 CPO에 대해서 정의된다고 하셨던 것으로 기억하는데 그러면 "Let D and D# be related by Galois connection" 이라는 조건이 주어지면 별다른 언급 없이도 D와 D# 모두 CPO라고 할 수 있나요?

Galois connection은 D와 D#이 poset이기만 하면 정의할 수 있습니다. 추가적인 조건이 있어야 합니다.

[EunsuKim03]

앗 감사합니다!