매칭 논리

일치 논리는 주로 컴퓨터 프로그램의 정확성에 대해 추론하는 데 사용되는 형식 논리입니다.연산자는 패턴 매칭을 사용하여 상태 집합이 아닌 상태의 전력 집합에서 작동합니다.이것은 그리고르 로주에 의해 만들어졌고 K 프레임워크에서 사용됩니다.

개요

일치 논리는 ^[1]패턴에서 작동합니다.문은 true 또는 false가 아닌 "일치하는" 값 집합으로 평가됩니다.

일련의 시그니처 ${displaystyle \Sigma$가 주어지면 패턴은 다음과 같습니다.

• 변수: $x{\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle \mathrm{Var}}$ ${\displaystyle$ x$\in$Var}
• 다른 패턴을 사용하는 시그니처 $\sigma {\displaystyle }$$σ$ \displaystyle \${\displaystyle {}_{}}$ \$in \Sigma}$ 다음$$ 구조:${\displaystyle }$σ (${\displaystyle {p1\mathrm{}}_{}}$ ${\displaystyle {p2\mathrm{}}_{},}$ ${\displaystyle .,}$ ${\displaystyle {pn}_{}}$ $){{displaystyle \sigma (p_{1}, p_{2},$ ..., $p_{n}}$
• 다른 패턴의 보완: $\neg {\displaystyle \mathrm{}}$ {\$displaystyle \negp}$
• 두 패턴의 교차점: ${\displaystyle {p\mathrm{}}_{}}$ 1${\displaystyle {}_{}}$∧ ${\displaystyle {p\mathrm{}}_{}}$2 \ $displaystyle p_{1}\land$ p_${2}$
• 바인딩: $∈$${\displaystyle x}$ .$$ {\$displaystyle \exists$x.$p}$와 x ${\displaystyle \exists }$ ${\displaystyle \mathrm{Var}}$ {\$displaystyle$ x$\in$Var}

일치하는 논리에는 S$({displaystyle$S})의 $종류$가 있을 수도 있습니다.이 경우 각 패턴은 특정 정렬에 속합니다.구조는 다른 종류의 패턴을 함께 결합하는 데 사용될 수 있습니다.프로그램 시맨틱을 사용할 때 사용되는 정렬의 예로는 "32비트 정수 값", "스택 프레임" 또는 "히프 메모리"가 있습니다.

일부 파생된 개념은 다음과 같이 정의됩니다.

• ${\displaystyle \top \equiv \displayx.x}$
• ${\displaystyle \bot \equiv \neg \top} 표시$
• ${\displaystyle p_{1}\lor p_{2}\equiv \neg (\neg p_{1}\land \neg p_{2})}$
• ${\displaystyle p_{1}\displaystyle p_{2}\equiv \neg p_{1}\lor p_{2}}$
• ${\displaystyle p_{1}\왼쪽 화살표 p_{2}\equiv p_{1}\implies p_{2}\land p_{2}\implies p_{1}}$
• ${\displaystyle \for all x.p\equiv \neg (\displaystyle x.\neg p)}$

${\displaystyle }$모든 요소가 {\$displaystyle \top}$과(와) 일치합니다$.$${\displaystyle }${\$displaystyle \bot}$이(가) 일치하지 않습니다$.$

"기본적인 직관이 ^[1]속을 수 있기 때문에 그러한 비고전적인 논리로 추론할 때는 조심해야 합니다."

일치하는 논리를 해석할 때(즉, 의미적 의미를 정의할 때) 패턴은 멱집합으로 모델링됩니다.문의 해석은 패턴과 일치하는 값의 집합입니다.

μ-Logic 일치

μ${displaystyle \mu}$ -logic을$$ $일치$시키면 고정점 $연산자{\displaystyle }$μ{$displaystyle \mu$^[2]가 추가됩니다.

적용들

일치 논리는 K 프레임워크에 의해 도달 가능성^[3] 논리와 함께 사용되어 작동 의미론을 지정하고 이로부터 호어 논리를 생성합니다.

일치 논리는 동일성을 갖는 1차 논리로 변환될 수 있으며, 이를 통해 K Framework는 기존 SMT 해결사를 사용하여 정리에 대한 증명을 찾을 수 있습니다.

참고 항목

• 분리 논리
• 호어 논리
• 문자열 집합과 일치하는 정규식

레퍼런스