개요
갈루아 대응 (Galois connection)은 Partial order set의 관계를 묘사한 이론이다.
간략하게 프로그램적인 지식으로 설명하면, 변조된 데이터로부터 절대 원래 데이터를 완벽하게 복구할 수 없다는 이론이다. 예를 들어서 손실 압축후에는 원본 파일을 완벽하게 복구하는 것은 불가능하다.
[math]D\Leftrightarrow D^{'}[/math] 란 관계가 있다고 해보자. D와 D'는 Partial order set이다.
[math]a\in D \rightarrow D^{'}[/math]는 Abstraction fucntion으로 정의하고,
[math]r\in D^{'} \rightarrow D[/math]를 Concretization function이라고 정의하자.
그러면 다음과 같은 [math]\forall x \in D, x^{'} \in D^{'}. a(x) \sqsubseteq x^{'} \Leftrightarrow r(x^{'})[/math]
정의가 반드시 성립한다.
이용
Abstract interpretation에서, 프로그램의 분석을 위해서는 Abstract domain을 정의하고 Concrete domain으로부터 Abstract domain으로 가는 Domain을 정의하게 된다. 이떄 갈루아 이론을 이용하면, Concrete domain에서 적용하는 법칙들 (예를 들면 Fixed point)이 Abstract domaion에서도 적용되고 최종적으로 Abstract domain에서 증명해도 Sound 함을 보일 수 있다.