문서 편집 권한이 없습니다. 다음 이유를 확인해주세요: 요청한 명령은 다음 권한을 가진 사용자에게 제한됩니다: 사용자. 문서의 원본을 보거나 복사할 수 있습니다. [[분류: 프로그램 분석]] == 개요 == 갈루아 대응 (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 함을 보일 수 있다. == 참고 == # https://en.wikipedia.org/wiki/Galois_connection 갈루아 대응 문서로 돌아갑니다.