프로그램 합성

컴퓨터 과학에서, 프로그램 합성은 주어진 높은 수준의 공식 규격을 입증할 수 있는 프로그램을 구성하는 작업이다.프로그램 검증과는 대조적으로 프로그램은 주어지는 것이 아니라 구성되어야 한다. 그러나 두 분야 모두 공식적인 입증 기술을 사용하며, 둘 다 다른 수준의 자동화 접근방식으로 구성되어 있다.자동 프로그래밍 기법과 달리, 프로그램 합성에서의 명세서는 보통 적절한 논리 ^[1]미적분에서의 비알고리즘 문장이 됩니다.

기원.

1957년 코넬 대학의 여름 기호 논리 연구소 동안, Alonzo Church는 수학적 ^[2]요건으로부터 회로를 합성하는 문제를 정의했습니다.비록 이 연구가 프로그램이 아닌 회로만을 언급하고 있지만, 이 연구는 프로그램 합성에 대한 최초의 기술 중 하나로 간주되며, 일부 연구자들은 프로그램 합성을 "처치의 문제"라고 부른다.1960년대에 인공지능 ^{[citation needed]}연구자들에 의해 "자동 프로그래머"에 대한 비슷한 아이디어가 연구되었다.

그 이후로, 다양한 연구 커뮤니티는 프로그램 합성 문제를 고려했다.주목할 만한 작품으로는 1969년 Büchi와 Landweber의 ^[3]오토마타 이론 접근법과 Manna와 Waldinger의 작품(1980년경)이 있다.현대의 고급 프로그래밍 언어의 발달은 프로그램 합성의 한 형태로도 이해될 수 있다.

21세기의 발전

21세기 초에는 공식 검증 커뮤니티와 관련 분야에서 프로그램 합성 아이디어에 대한 실질적인 관심이 급증했다.Armando Solar-Lezama는 부울 로직으로 프로그램 합성 문제를 인코딩하고 ^[4]부울 만족도 문제를 위한 알고리즘을 사용하여 프로그램을 자동으로 찾을 수 있음을 보여주었다.2013년에는 UPenn, UC Berkeley 및 ^[5]MIT의 연구진에 의해 프로그램 합성 문제에 대한 통합 프레임워크가 제안되었으며, 2014년부터 SyGuS-Comp라는 ^[6]경쟁 행사에서 프로그램 합성을 위한 다양한 알고리즘을 비교하는 프로그램 합성 대회가 매년 개최되고 있습니다.그러나 사용 가능한 알고리즘은 작은 프로그램만 합성할 수 있습니다.

마나와 월딩거의 틀

비박해 결의 규칙(대체 단일화는 제시되지 않음)

Nr	어설션	목표들	프로그램.	기원.
51	${\displaystyle E[p]}$
52	${\displaystyle F[p]}$
53		${\displaystyle G[p]}$	s
54		${\displaystyle H[p]}$	t
55	$\displaystyle E[{\text{true}}}\lor F[{\text{false}}}}]$			해결(51,52)
56		$\displaystyle \lnot F[{\text{true}}}\land G[{\text{false}}}}$	s	해결(52,53)
57		$\displaystyle \lnot F[{\text{false}}}\land G[{\text{true}}}}$	s	해결(53,52)
58		$\displaystyle G[{\text{true}}}\land H[{\text{false}}}}]$	p ? s : t	해결(53,54)

1980년에 ^[7][8]발표된 Manna and Waldinger의 프레임워크는 사용자가 지정한 1차 사양 공식에서 출발합니다.그 공식에 대해 증명서가 구축되어 치환을 통일하여 기능 프로그램을 합성한다.

프레임워크는 표 레이아웃으로 표시됩니다.열에는 다음이 포함됩니다.

• 참조용 회선번호("Nr")
• 이미 확립된 공식(공리 및 전제조건 포함)
• 사후 조건('목표')^{[note 1]}을 포함하여 아직 입증되지 않은 공식
• 유효한 출력값("프로그램")^{[note 2]}을 나타내는 용어
• 현재 행('Origin')의 자리 매김

처음에 배경 지식, 전제 조건 및 사후 조건이 표에 입력됩니다.그 후 적절한 증명 규칙을 수동으로 적용합니다.이 프레임워크는 중간 공식의 인간 가독성을 향상시키도록 설계되었다. 고전적 분해능과는 달리, 클래설 정규 형식을 필요로 하지 않지만 임의 구조의 공식으로 추론할 수 있고 접합자를 포함할 수 있다("비클래설 분해능").${\displaystyle \mathit{증명}}$은 [Goals$]$컬럼 또는 [Assessions$]$${\displaystyle \mathit{컬럼}}$에 [$](표시$ $스타일$$)$이 $있으면{\displaystyle \mathit{}}$ $완료$됩니다.이 접근법에 의해 취득된 프로그램은, 최초로 개시된 사양식을 만족시키는 것이 보증됩니다.이러한 의미에서,^[9] 이러한 의미에서는, 그것들은 구조적으로 정확합니다.조건부, 재귀, 산술 및 기타^{[note 3]} 연산자로 구성된 튜링 완전,^[10] 순수 기능적 프로그래밍 언어만 지원됩니다.이 프레임워크 내에서 수행된 사례 연구는 예를 들어 나눗셈,^[11] 나머지,^[12] 제곱근, 용어 통일,^[13] 관계형 데이터베이스^[14] 쿼리에 대한 응답 및 여러 정렬 ^[15][16]알고리즘을 계산하기 위해 알고리즘을 통합했다.

증명 규칙

증명 규칙은 다음과 같습니다.

• 비클래션 해결(표 참조).

예를 들어, 55행은 51부터 Assertion $공식{\displaystyle }$ E$(표시 스타일$ E$)$와 52부터 F$(표시 스타일$ F$)$를 해결하여 얻을 수 있으며, 둘 다 공통 보조 $공식{\displaystyle }$ p$(표시 스타일$ p$)$를 공유합니다.리졸벤트는 E$($$디스플레이$ 스타일)의 분리로 형성되며, ${\displaystyle \mathit{p}}$$(\displaystyle$ p$)$는 ${\displaystyle \mathit{tru}}$ e$(\displaystyle$ {$true})$로,$$F(\$displaystyle$ F$)$는$$$(\display$ $style$ p$)$로 바뀝니다.이 리졸벤트는 논리적으로$$E(\$displaystyle$ $E$)와 F(\$displaystyle$F)의 조합에 따라 이루어집니다.일반적으로 E$(\displaystyle$ E$)$와 F$(\displaystyle$ F$)$에는 각각 2개의 Uniformal $subformula{\displaystyle {}_{}}$ $(\$과 $(\$만 있으면 됩니다.그런 다음 이전과 같이 E ${\$ { $displaystyle$E \$theta$} 및$$ $F{\displaystyle }$ ${\$ { $displaystyle$F \$theta$} 로 $구성$됩니다.$여기$서 $\displaystyle \theta }$는 p$$ { $displaystyle p_{1$} 및$$ ${\displaystyle {p\mathrm{}}_{}}$2 {$displaystyle p_{2$ 의 $가장{\displaystyle {}_{}}$ 일반적인 통일체입니다.이 규칙은 ^[17]절을 일반화합니다.

부모 공식의 프로그램 용어를 라인 58과 같이 조합하여 분해능의 출력을 형성한다.일반적인 경우, $후자$에도 $§(\displaystyle\theta)$가 적용됩니다.출력에 서브포뮬라$p{\displaystyle }$\$displaystyle$p가$$ 표시되므로 계산 가능한 속성에 대응하는 서브포뮬라에서만 해결할 수 있도록 주의해야 합니다.

• 논리 변환

예를 들어, E${\displaystyle f}$ ( F${\displaystyle )}$ G$$) \ $displaystyle E\land$( F \$lor$G$$ ) (${\displaystyle }$（ E${\displaystyle g}$F ）$$（ $E$ \ $displaystyle$( E \$land$F ) $\lor$( E \$land$G )로 변환할 수 ${\displaystyle \mathrm{있습니다}}$.${\displaystyle \mathrm{이것}}$은, 양쪽 모두, 골에 상당하기 때문입니다.

• 연결 주장과 연결 목표의 분할.

아래의 장난감 예제의 11~13행에 예가 나와 있습니다.

• 구조 유도.

이 규칙에 따라 재귀 함수를 통합할 수 있습니다.${\displaystyle \mathit{\text{주어진}}}$ 사전 및 사후 $조건$의 경우${\displaystyle }$(${\displaystyle x})$ (x)${\displaystyle }$(x$$$)$ (x) ($x)$ (x) (${\displaystyle x)}$ $=$(${\displaystyle x)}$ (x) (${\displaystyle \mathit{\text{x}}}$) (x) ($x,$ y) (x, y) (x, y) (x, y) (x, y)$$(x, y) (x, y) (x, y) (x$$, y) (x$,$ y) ($x{\displaystyle }$) (x) (x) ($x,$ y$){\displaystyle }$ (x) (x, y${\displaystyle )}$ (x) (x, ${\displaystyle y}$)) ($x$$,$ y$)$ (x) (x) (x) (x) (x) (x) (x")′≺)∧ 제작()′)⟹ 포스트()′, f()′)){\displaystylex'\prec x\land{\textit{제작}}()의)\implies{\textit{포스트}}(x',f(x'))}"[18]이 주장을 가지고서 해결하는 귀납적인 호출이 프로그램에{\displaystyle f}f에게 소개할 수 있는 메인 x{\displaystyle)}의, 그것은 항상 Assertion을 추가하기 위해 건전하다.착륙m.

예를 들어 Manna, Waldinger(1980), ${\displaystyle {}^{}}$ 108-111에 나타나 여기서 0n n${\displaystyle }$ n < n $style$ ( n ,d '$)\display$style ( $n$' ,$d$ ' $)\prec$( n ,$$d${\displaystyle }$)를 $사용$하여 주어진 $2개$의 정수의 몫과 나머지를 계산하는 알고리즘이 합성됩니다.

Murray는 이 규칙들이 1차 ^[19]논리에 완전하다는 것을 보여 주었다.1986년, Manna와 Waldinger는 ^[20]평등을 다루기 위해 일반화된 E-해상도 및 매개변조 규칙을 추가했다; 나중에, 이 규칙들은 불완전하다는 것이 판명되었다.^[21]

예

최대 함수의 합성 예

Nr	어설션	목표들	프로그램.	기원.
1	${\displaystyle A=A}$			공리
2	${\displaystyle A\leq A}$			공리
3	$(\displaystyle A\leq B\lor B\leq A)$			공리
10		$({displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}$	M	사양
11		${\displaystyle(x\leq M\leq M\land x=M)\lor(x\leq M\land y\leq M\land y=M)}$	M	왜곡(10)
12		${\displaystyle x\leq M\leq M\leq M\land x=M}$	M	분할(11)
13		${\displaystyle x\leq M\leq M\leq M\land y=M}$	M	분할(11)
14		${\displaystyle x\leq x\land y\leq x}$	x	해결(12,1)
15		${\displaystyle y\leq x}$	x	해결(14,2)
16		$\displaystyle \lnot (x\leq y)$	x	해결(15,3)
17		$(\displaystyle x\leq y\land y\leq y)$	y	해결(13,1)
18		${\displaystyle x\leq y}$	y	해결(17,2)
19		${\displaystyle {true}}$	x <y? y : x	해결(18,16)

장난감의 예로서 x$(\displaystyle$x)와 y$(\displaystyle$ y$)$의 최대$$ M$(\displaystyle$ M$)$을 계산하는 함수 프로그램은 ^{[citation needed]}다음과 같이 도출할 수 있습니다.

요건 설명 "최대값은 주어진 수보다 크거나 같으며 주어진 수 중 하나"에서 시작하여 1차 공식${\displaystyle \mathrm{}x}$ X${\displaystyle \mathrm{}y}$ Y${\displaystyle m}$ M : X${\displaystyle m}$ Y${\displaystyle m}$ M ∧ M ${\displaystyle \wedge }$ ${\displaystyle M}$ ∧ ( ${\displaystyle X}$ ${\displaystyle =}$ ${\displaystyle M}$ ${\displaystyle \vee }$ $Y$ ${\displaystyle =}$M )$$\ style \ $for$X : \ $ex$ \ $all$ \ ） 。이 공식은 증명될 것이다.역스콜렘화에 ^{[note 4]}의해 10행의 사양, 변수를 나타내는 대소문자와 스콜렘 상수를 얻는다.

11행의 분배법칙에 대한 변환규칙을 적용한 후 증명목표는 분리가 되기 때문에 viz라는 두 가지 경우로 나눌 수 있다.12행과 13행.

첫 번째 경우는 1행의 공리로 12행을 해결하면 14행의 프로그램 $변수{\displaystyle }$ M$(\displaystyle$ M$)$이 인스턴스화된다.직감적으로 12행의 마지막 접속사는 이 경우$$M(\$displaystyle$M)이$$ $취해야{\displaystyle }$ 할 값을 규정합니다.형식적으로, 위의 57행에 표시된 비박해 결의 규칙은 12행과 1행에 적용된다.

• p는 A=A 및 x=M의 공통 인스턴스 x=x이며, 후자의 공식을 구문적으로 통일하여 구한다.
• F[p]는 참 x x=x이며 인스턴스화된 라인 1(p 주위의 컨텍스트 F[context]를 표시하도록 패딩됨)에서 얻을 수 있다.
• G[p]는 x x x y y x x x x x x = x이며, 인스턴스화 선 12에서 구한다.

$(\displaystyle \lnot (}$ true$$ ${\displaystyle \mathrm{false}}$ false) ($x$${\displaystyle }$" x " y " " ${\displaystyle x}$ " ${\displaystyle }$ true$$) (\$displaystyle$$$x$\leq x\land$y\$leq$x$$) $)$를 나타냅니다.

마찬가지로 라인 14는 라인 15를 산출하고 다음으로 라인 16을 분해능으로 산출한다.또, 라인 13의 제2의 케이스 x${\displaystyle m}$ M${\displaystyle y}$ y${\displaystyle m}$ M${\displaystyle y}$ y ${\displaystyle =}$ { $displaystyle$ x$\leq M\land$ y$=M$}도 $동일하게 취급되어 최종적으로 라인$18이 된다.

마지막 단계에서 라인 58로부터의 해결 규칙을 사용하여 두 케이스(즉, 라인 16 및 18)를 결합한다.이 규칙을 적용하기 위해서는 준비 스텝 15→16이 필요했다.직감적으로 라인 18은 "${\$ ${\displaystyle y}$ \ $displaystyle$$$x \ $leq$y$"$로 해석할 수 있으며$,$ 라인 15는 "y$style$ x \ $displaystyle y\$leq x$"$로 출력 x$\displaystyle$x가$$ 유효하며, 스텝 15→16은 케이스 16과 케이스 18을 모두 확립합니다.상호보완적입니다.^{[note 5]}16행과 18행 모두 프로그램 용어를 포함하므로 조건식이 프로그램 열에 표시됩니다.목표$true$가 도출되었기$$ 때문에 증명은 완료되고 $true$$행$의 프로그램 컬럼에는 프로그램이 포함됩니다.

「 」를 참조해 주세요.

• 유도 프로그래밍
• 메타프로그래밍
• 프로그램 파생
• 자연어 프로그래밍
• 반응 합성

메모들

레퍼런스

• Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis". Artificial Intelligence. 6 (2): 175–208. doi:10.1016/0004-3702(75)90008-9.