갈루아 대응 - 편집 역사

Ahn9807: /* 이용 */

2023-11-14T03:21:01Z

이용

← 이전 판		2023년 11월 14일 (화) 03:21 판
18번째 줄:		18번째 줄:

	== 이용 ==		== 이용 ==
	[[Abstract interpretation]]에서, 프로그램의 분석을 위해서는 Abstract domain을 정의하고 Concrete domain으로부터 Abstract domain으로 가는 Domain을 정의하게 된다. 이떄 갈루아 이론을 이용하면, Concrete domain에서 적용하는 법칙들 (예를 들면 [[Fixed point]])이 Abstract domaion에서도 적용되고 최종적으로 Abstract domain에서 증명해도 Sound 함을 보일 수 있다.		[[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		# https://en.wikipedia.org/wiki/Galois_connection

2023년 11월 13일 (월) 06:03에 Ahn9807님의 편집

2023-11-13T06:03:19Z

← 이전 판		2023년 11월 13일 (월) 06:03 판
19번째 줄:		19번째 줄:
	== 이용 ==		== 이용 ==
	[[Abstract interpretation]]에서, 프로그램의 분석을 위해서는 Abstract domain을 정의하고 Concrete domain으로부터 Abstract domain으로 가는 Domain을 정의하게 된다. 이떄 갈루아 이론을 이용하면, Concrete domain에서 적용하는 법칙들 (예를 들면 [[Fixed point]])이 Abstract domaion에서도 적용되고 최종적으로 Abstract domain에서 증명해도 Sound 함을 보일 수 있다.		[[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		# https://en.wikipedia.org/wiki/Galois_connection

Ahn9807: 새 문서: 분류: 프로그램 분석 == 개요 == 갈루아 대응 (Galois connection)은 Partial order set의 관계를 묘사한 이론이다. 간략하게 프로그램적인 지식으로 설명하면, 변조된 데이터로부터 절대 원래 데이터를 완벽하게 복구할 수 없다는 이론이다. 예를 들어서 손실 압축후에는 원본 파일을 완벽하게 복구하는 것은 불가능하다. $D\Leftrightarrow D^{'}$ 란 관계가 있다고...

2023-11-13T06:03:09Z

새 문서: 분류: 프로그램 분석 == 개요 == 갈루아 대응 (Galois connection)은 Partial order set의 관계를 묘사한 이론이다. 간략하게 프로그램적인 지식으로 설명하면, 변조된 데이터로부터 절대 원래 데이터를 완벽하게 복구할 수 없다는 이론이다. 예를 들어서 손실 압축후에는 원본 파일을 완벽하게 복구하는 것은 불가능하다. <math>D\Leftrightarrow D^{'}</math> 란 관계가 있다고...

새 문서

[[분류: 프로그램 분석]]

== 개요 ==
갈루아 대응 (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