목표와 절

논리 프로그래밍 용어로, 목표(goal)는 증명해야 하는 것이고 절(clause)은 참이라고 알고 있는 것입니다. 논리로의 로워링 장에서 설명한 것처럼, Rust의 트레이트 솔버는 hereditary harrop(HH) 절을 확장한 것에 기반하며, HH 절은 전통적인 Prolog 혼 절에 몇 가지 새로운 강력한 기능을 더한 것입니다.

목표와 절의 메타 구조

Rust의 솔버에서 목표와 절은 다음과 같은 형태를 가집니다(두 정의가 서로를 참조한다는 점에 유의하십시오).

Goal = DomainGoal           // defined in the section below
        | Goal && Goal
        | Goal || Goal
        | exists<K> { Goal }   // existential quantification
        | forall<K> { Goal }   // universal quantification
        | if (Clause) { Goal } // implication
        | true                 // something that's trivially true
        | ambiguous            // something that's never provable

Clause = DomainGoal
        | Clause :- Goal     // if can prove Goal, then Clause is true
        | Clause && Clause
        | forall<K> { Clause }

K = <type>     // a "kind"
    | <lifetime>

이러한 종류의 목표에 대한 증명 절차는 사실 매우 간단합니다. 본질적으로 이는 깊이 우선 탐색의 한 형태입니다. 자세한 내용은 논문 “A Proof Procedure for the Logic of Hereditary Harrop Formulas”에 나와 있습니다.

코드 측면에서 이 타입들은 rustc에서는 rustc_middle/src/traits/mod.rs에, chalk에서는 chalk-ir/src/lib.rs에 정의되어 있습니다.

도메인 목표

도메인 목표는 트레이트 논리의 원자입니다. 위에 제시한 정의에서 볼 수 있듯이, 일반 목표는 기본적으로 도메인 목표들의 조합으로 이루어집니다.

또한 앞서 제시한 절의 정의를 조금 평탄화해 보면, 절은 항상 다음과 같은 형태임을 알 수 있습니다.

forall<K1, ..., Kn> { DomainGoal :- Goal }

따라서 도메인 목표는 사실 절의 좌변(LHS)입니다. 즉, 가장 세분화된 수준에서 도메인 목표는 트레이트 솔버가 최종적으로 증명하려고 시도하게 되는 대상입니다.

우리 시스템의 도메인 목표 집합을 정의하려면 먼저 몇 가지 간단한 공식을 소개해야 합니다. 트레이트 참조(trait reference)는 트레이트의 이름과 그에 알맞은 입력 집합 P0..Pn으로 구성됩니다.

TraitRef = P0: TraitName<P1..Pn>

예를 들어 u32: Display는 트레이트 참조이며, Vec<T>: IntoIterator도 마찬가지입니다. Rust 표면 구문은 연관 타입 바인딩(Vec<T>: IntoIterator<Item = T>)처럼 트레이트 참조에 속하지 않는 몇 가지 추가 요소도 허용한다는 점에 유의하십시오.

프로젝션(projection)은 연관 항목 참조와 그 입력 P0..Pm으로 구성됩니다.

Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>

이를 바탕으로 DomainGoal을 다음과 같이 정의할 수 있습니다.

DomainGoal = Holds(WhereClause)
            | FromEnv(TraitRef)
            | FromEnv(Type)
            | WellFormed(TraitRef)
            | WellFormed(Type)
            | Normalize(Projection -> Type)

WhereClause = Implemented(TraitRef)
            | ProjectionEq(Projection = Type)
            | Outlives(Type: Region)
            | Outlives(Region: Region)

WhereClause는 Rust 사용자가 Rust 프로그램에서 실제로 작성할 수 있는 where 절을 가리킵니다. 이 추상화는 Rust에서 실제로 작성 가능한 도메인 목표만 다루고 싶을 때가 있기 때문에 오직 편의를 위해 존재합니다.

이제 이들 각각을 하나씩 살펴봅시다.

Implemented(TraitRef)

예: Implemented(i32: Copy)

주어진 트레이트가 주어진 입력 타입과 라이프타임에 대해 구현되어 있으면 참입니다.

ProjectionEq(프로젝션 = 타입)

예: ProjectionEq<T as Iterator>::Item = u8

주어진 연관 타입 Projection은 Type과 같습니다. 이는 정규화를 사용하거나 플레이스홀더 연관 타입을 사용하여 증명할 수 있습니다. Chalk Book의 연관 타입 절을 참조하십시오.

Normalize(프로젝션 -> 타입)

예: ProjectionEq<T as Iterator>::Item -> u8

주어진 연관 타입 Projection을 Type으로 정규화할 수 있습니다.

Chalk Book의 연관 타입 절에서 설명한 것처럼, Normalize는 ProjectionEq를 함의하지만 그 역은 성립하지 않습니다. 일반적으로 Normalize(<T as Trait>::Item -> U)를 증명하려면 Implemented(T: Trait)도 증명해야 합니다.

FromEnv(TraitRef)

예: FromEnv(Self: Add<i32>)

내부의 TraitRef가 참이라고 가정되는 경우, 즉 스코프 내 where 절로부터 유도될 수 있는 경우에 참입니다.

예를 들어, 다음과 같은 함수가 있다고 합시다.

#![allow(unused)]
fn main() {
fn loud_clone<T: Clone>(stuff: &T) -> T {
    println!("cloning!");
    stuff.clone()
}
}

이 함수의 본문 안에서는 FromEnv(T: Clone)이 성립합니다. 스코프 내 where 절은 중첩되므로, impl 본문 안에 있는 함수 본문은 impl 본문의 where 절도 상속합니다.

이 규칙과 다음 규칙은 암시적 바운드를 구현하는 데 사용됩니다. 로워링 절에서 살펴보겠지만, FromEnv(TraitRef)는 Implemented(TraitRef)를 함의하지만 그 역은 성립하지 않습니다. 이 구분은 암시적 바운드에 매우 중요합니다.

FromEnv(Type)

예: FromEnv(HashSet<K>)

내부의 Type이 적격하다고 가정되는 경우, 즉 함수나 impl의 입력 타입인 경우 참입니다.

예를 들어, 다음 코드가 있다고 합시다.

struct HashSet<K> where K: Hash { ... }

fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
    println!("inserting!");
    set.insert(item);
}

HashSet<K>는 loud_insert 함수의 입력 타입입니다. 따라서 우리는 이것이 적격하다고 가정하며, 그러므로 함수 본문 내부에서 FromEnv(HashSet<K>)를 가지게 됩니다. 로워링 절에서 살펴보겠지만, HashSet 선언이 K: Hash where 절과 함께 작성되었기 때문에 FromEnv(HashSet<K>)는 Implemented(K: Hash)를 함의합니다. 따라서 loud_insert 함수에 그 바운드를 반복해서 적을 필요가 없습니다. 오히려 그 바운드가 참이라고 자동으로 가정합니다.

WellFormed(Item)

이 목표들은 주어진 항목이 적격하다는 것을 함의합니다.

다양한 종류의 항목이 적격하다는 것에 대해 이야기할 수 있습니다.

타입: 예를 들어 WellFormed(Vec<i32>)는 Rust에서 참이지만, WellFormed(Vec<str>)는 참이 아닙니다(str이 Sized가 아니기 때문입니다).
TraitRef: 예를 들어 WellFormed(Vec<i32>: Clone)이 있습니다.

적격성은 암시적 바운드에 중요합니다. 특히 loud_clone 예제에서 FromEnv(T: Clone)을 가정해도 괜찮은 이유는 loud_clone의 각 호출 지점마다 WellFormed(T: Clone)도 검증하기 때문입니다. 마찬가지로 loud_insert 예제에서 FromEnv(HashSet<K>)를 가정해도 괜찮은 이유는 loud_insert의 각 호출 지점마다 WellFormed(HashSet<K>)를 검증하기 때문입니다.

Outlives(Type: Region), Outlives(Region: Region)

예: Outlives(&'a str: 'b), Outlives('a: 'static)

왼쪽에 주어진 타입 또는 리전이 오른쪽 리전보다 오래 살아남으면 참입니다.

공귀납적 목표

우리 시스템의 목표는 대부분 “귀납적“입니다. 귀납적 목표에서는 순환 추론이 허용되지 않습니다. 다음 예시 절을 살펴보십시오.

    Implemented(Foo: Bar) :-
        Implemented(Foo: Bar).

귀납적으로 고려하면 이 절은 쓸모가 없습니다. Implemented(Foo: Bar)를 증명하려고 하면 재귀적으로 Implemented(Foo: Bar)를 증명해야 하고, 그 순환은 끝없이 계속될 것이기 때문입니다(트레이트 솔버는 여기서 종료되며, 단지 Implemented(Foo: Bar)가 참인지 알 수 없다고 간주할 것입니다).

그러나 일부 목표는 공귀납적입니다. 간단히 말해, 이는 순환이 허용된다는 뜻입니다. 따라서 Bar가 공귀납적 트레이트라면 위의 규칙은 완벽하게 유효하며, Implemented(Foo: Bar)가 참임을 나타냅니다.

자동 트레이트는 Rust에서 공귀납적 목표가 사용되는 한 가지 예입니다. Send 트레이트를 살펴보고, 다음과 같은 구조체가 있다고 가정해 보십시오.

#![allow(unused)]
fn main() {
struct Foo {
    next: Option<Box<Foo>>
}
}

자동 트레이트의 기본 규칙에 따르면, Foo의 필드 타입들이 Send이면 Foo는 Send입니다. 따라서 다음과 같은 규칙이 생깁니다.

Implemented(Foo: Send) :-
    Implemented(Option<Box<Foo>>: Send).

짐작하시겠지만, Option<Box<Foo>>: Send를 증명하다 보면 결국 순환적으로 Foo: Send를 다시 증명해야 하게 됩니다. 따라서 이는 순환에 빠지게 되는 예이지만, 괜찮습니다. Foo: Send가 자기 자신을 참조하더라도 우리는 이것이 성립한다고 실제로 간주합니다.

일반적으로 공귀납적 트레이트는 Rust 트레이트 해결에서 고정된 가능성의 집합을 열거하고자 할 때 사용됩니다. 자동 트레이트의 경우, 주어진 시작점에서 도달 가능한 타입의 집합을 열거합니다(즉, Foo는 Option<Box<Foo>> 타입의 값에 도달할 수 있고, 이는 Box<Foo> 타입의 값에, 그리고 다시 Foo 타입의 값에 도달할 수 있음을 의미하며, 이로써 순환이 완성됩니다).

자동 트레이트 외에도 WellFormed 술어는 공귀납적입니다. 이들은 암시적 바운드에 관한 절에서 설명한 것처럼, 비슷한 “모든 경우 열거” 패턴을 구현하는 데 사용됩니다.

미완성 장

아직 작성되지 않은 주제는 다음과 같습니다.

증명 절차에 대한 상세 설명
SLG 해결 – 부정 추론 도입

Keyboard shortcuts

Rust 컴파일러 개발 가이드