program semantics를 정의할 때 poset, CPO, lattice, complete lattice 같은 순서 구조가 필요한 이유는 크게 두 가지입니다:

1. 정보의 크기 비교

   프로그램의 의미를 "가능한 상태들의 집합"이나 "정보량"으로 모델링할 때, 이들 사이에 어느 쪽이 더 정밀한지(많은 정보를 담고 있는지)를 비교할 수 있어야 합니다. 이때 자연스럽게 부분순서(poset)를 도입합니다. 예를 들어, 집합 포함 관계(⊆)는 "어떤 상태 집합이 다른 집합보다 더 많은 실행을 포함한다"는 의미로 쓰입니다.

2. 루프의 의미 = 고정점 문제

   루프(while 등)의 의미는 수학적으로 연산자의 least fixpoint로 정의됩니다. 이 고정점이 항상 존재한다는 것을 보장하려면 순서구조가 충분히 풍부해야 합니다.

   • Tarski의 정리: 완비 격자(complete lattice) 위의 단조 연산자는 항상 least fixpoint를 갖습니다.

   • Kleene의 정리: CPO(모든 chain에 대해 lub가 존재하는 poset) 위의 연속 연산자는 least fixpoint를 반복(iteration) 극한으로 구할 수 있습니다.

     따라서 CPO나 complete lattice는 루프 semantics를 수학적으로 잘 정의하기 위한 필수 기반입니다.

정리하면:

• poset: 정보의 정밀도를 비교하기 위해 필요.
• CPO / complete lattice: 루프의 의미를 least fixpoint로 정의하고, 그 존재성과 계산 가능성을 보장하기 위해 필요.

즉, 순서가 있는 집합 구조는 프로그램의 semantics를 수학적으로 엄밀히 정의하고, 특히 반복/루프 구조에서 의미가 잘 정의되도록 하는 데 핵심적인 역할을 합니다.