1314.11 전칭 양화 전제 조건과 forall 연산자

1314.11 전칭 양화 전제 조건과 forall 연산자

1. 전칭 양화의 정의

전칭 양화(universal quantification)는 특정 타입의 모든 객체에 대해 주어진 조건이 성립할 것을 요구하는 논리적 구성이다. PDDL에서 전칭 양화는 forall 연산자로 표현되며, :universal-preconditions 또는 :adl 요구사항의 활성화가 필요하다.

구문은 다음과 같다:

(forall (<typed-variable-list>) <formula>)

형식적 의미론은 다음과 같이 정의된다:

s \models (\text{forall} \ (?x - T) \ \phi(?x)) \iff \forall o \in \text{objects}(T): s \models \phi[?x/o]

여기서 \text{objects}(T)는 타입 T에 속하는 모든 객체의 집합이고, \phi[?x/o]는 공식 \phi에서 변수 ?x를 객체 o로 대입한 결과이다. 타입 계층이 존재하는 경우, \text{objects}(T)는 T의 하위 타입에 속하는 객체도 포함한다.

2. 기본 활용 예시

2.1 모든 경로의 안전 확인

(:action traverse_corridor
    :parameters (?r - robot ?from - waypoint ?to - waypoint)
    :precondition (and
        (robot_at ?r ?from)
        (corridor ?from ?to)
        (forall (?obs - obstacle)
            (not (obstacle_in_corridor ?obs ?from ?to))
        )
    )
    :effect (and (not (robot_at ?r ?from)) (robot_at ?r ?to))
)

이 전제 조건은 출발지와 도착지 사이의 복도에 어떤 장애물도 존재하지 않을 것을 요구한다. forall 양화사는 모든 장애물 객체에 대해 순회하면서, 각 장애물이 해당 복도에 없음을 확인한다.

2.2 모든 센서의 정상 작동 확인

(:action start_autonomous_mode
    :parameters (?r - robot)
    :precondition (and
        (robot_initialized ?r)
        (forall (?s - sensor)
            (imply (sensor_on ?r ?s) (sensor_calibrated ?s))
        )
    )
    :effect (autonomous_mode ?r)
)

이 예시에서 forall과 imply의 결합은 “로봇에 장착된 모든 활성 센서가 보정(calibration)되어 있어야 한다“는 조건을 표현한다. 비활성 센서나 해당 로봇에 장착되지 않은 센서에 대해서는 imply의 전건이 거짓이므로 조건이 자동으로 충족��다.

3. forall과 imply의 결합 패턴

forall은 단독으로 사용되기보다 imply와 결합하여 조건부 전칭 제약을 표현하는 것이 일반적이다. 이 패턴의 형태는 다음과 같다:

(forall (?x - Type)
    (imply <guard-condition> <required-condition>)
)

이는 다음의 의미를 갖는다: “타입 Type의 모든 객체 x에 대해, guard-condition이 성립하면 required-condition도 성립해야 한다.”

형식적으로:

\forall x \in \text{objects}(T): \text{guard}(x) \Rightarrow \text{required}(x)

이 패턴이 필수적인 이유는, imply 없이 forall 내부에 직접 조건을 명시하면 해당 타입의 모든 객체에 대해 무조건적으로 조건이 성립해야 하기 때문이다:

;; 지나치게 강한 조건: 모든 문이 열려 있어야 함
(forall (?d - door) (door_open ?d))

;; 적절한 조건: 경로상의 문만 열려 있으면 됨
(forall (?d - door)
    (imply (door_on_path ?d ?from ?to) (door_open ?d))
)

4. 다중 변수 양화

forall 연산자는 동시에 여러 변수를 양화할 수 있다:

(:action clear_workspace
    :parameters (?r - robot ?ws - workspace)
    :precondition (and
        (robot_at ?r ?ws)
        (forall (?obj - movable_object ?loc - storage)
            (imply (object_in_workspace ?obj ?ws)
                (storage_available ?loc)
            )
        )
    )
    :effect (workspace_cleared ?ws)
)

다중 변수 양화에서 변수들의 바인딩은 데카르트 곱(Cartesian product)으로 전개된다:

\forall (x, y) \in \text{objects}(T_1) \times \text{objects}(T_2): \phi(x, y)

이는 \lvert\text{objects}(T_1)\rvert \times \lvert\text{objects}(T_2)\rvert개의 조건을 생성하므로, 변수 수와 객체 수에 따라 평가 비용이 급증할 수 있다.

5. 전칭 양화의 그라운딩

플래너 내부에서 forall 양화사는 접합(conjunction)으로 전개(unrolling)될 수 있다. 타입 T에 속하는 객체가 \{o_1, o_2, \ldots, o_m\}이면:

(\text{forall} \ (?x - T) \ \phi(?x)) \equiv (\text{and} \ \phi[?x/o_1] \ \phi[?x/o_2] \ \ldots \ \phi[?x/o_m])

이 전개는 양화사를 지원하지 않는 STRIPS 플래너에서 forall을 처리하는 표준적 방법이다. 그러나 객체 수가 많은 경우 전개된 접합의 크기가 매우 커질 수 있으며, 이는 플래닝 성능에 부정적 영향을 미친다.

예를 들어, 100개의 웨이포인트 객체가 존재하는 도메인에서 다음의 전제 조건:

(forall (?w - waypoint) (imply (on_route ?w) (clear ?w)))

은 100개의 함축 조건으로 전개된다. 각 조건의 평가에 상수 시간이 소요된다 해도, 전체 평가 비용은 O(m)이며, 이것이 모든 그라운드 액션에 대해 반복적으로 수행되면 상당한 계산 부하가 발생한다.

6. 중첩 양화

forall 양화사는 중첩이 가능하며, 중첩 깊이에 따라 표현력과 계산 복잡도가 모두 증가한다:

;; 2중 중첩 전칭 양화
(:action verify_all_connections
    :parameters (?network - comm_network)
    :precondition (and
        (network_active ?network)
        (forall (?n1 - node)
            (forall (?n2 - node)
                (imply (and (in_network ?n1 ?network)
                            (in_network ?n2 ?network)
                            (not (= ?n1 ?n2)))
                    (can_communicate ?n1 ?n2)
                )
            )
        )
    )
    :effect (network_verified ?network)
)

이 전제 조건은 네트워크 내의 모든 노드 쌍이 통신 가능할 것을 요구한다. 2중 중첩은 O(m^2)개의 조건으로 전개되며, 3중 이상의 중첩은 실용적 관점에서 피해야 한다.

7. 로봇 도메인에서의 전칭 양화 활용

7.1 다중 로봇 안전 간격 확인

(:action deploy_robot
    :parameters (?r - robot ?loc - waypoint)
    :precondition (and
        (robot_ready ?r)
        (forall (?other - robot)
            (imply (and (not (= ?other ?r)) (robot_deployed ?other))
                (safe_distance ?loc (position_of ?other))
            )
        )
    )
    :effect (and (robot_deployed ?r) (robot_at ?r ?loc))
)

7.2 작업 영역 내 모든 전제 조건 충족 확인

(:action begin_assembly
    :parameters (?r - robot ?product - assembly)
    :precondition (and
        (robot_at ?r assembly_station)
        (forall (?part - component)
            (imply (required_for ?part ?product)
                (part_available ?part assembly_station)
            )
        )
    )
    :effect (assembly_in_progress ?product)
)

이 전제 조건은 제품 조립에 필요한 모든 부품이 조립 스테이션에 준비되어 있을 것을 요구한다.

8. 설계 지침

  1. forall은 반드시 imply와 함께 사용하는 것을 기본으로 하라. 무조건적 전칭 양화는 지나치게 강한 제약을 생성하여 플래너가 유효한 계획을 찾지 못하게 할 수 있다.

  2. 양화 변수의 타입을 가능한 한 구체적으로 지정하라. 넓은 타입을 사용하면 불필요한 객체까지 양화 범위에 포함되어 평가 비용이 증가한다.

  3. 양화 내부의 조건을 단순하게 유지하라. 양화 내부에 복잡한 중첩 논리식을 배치하면 가독성과 플래닝 효율이 모두 저하된다.

  4. 중첩 깊이를 최소화하라. 2중 이상의 양화 중첩은 계산 비용이 급격히 증가하므로, 도메인 모델의 재설계를 통해 중첩을 줄이는 것이 바람직하���.

  5. 플래너 호환성을 확인하라. 일부 플래너는 forall의 전개(unrolling)에서 성능 저하를 경험할 수 있으므로, 대상 플래너의 양화사 처리 방식을 사전에 확인해야 한다.

9. 참고 문헌

  • Ghallab, M., Nau, D., & Traverso, P. (2004). Automated Planning: Theory and Practice. Morgan Kaufmann.
  • Pednault, E. P. D. (1989). “ADL: Exploring the Middle Ground Between STRIPS and the Situation Calculus.” Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR), 324–332.
  • Helmert, M. (2009). “Concise Finite-Domain Representations for PDDL Planning Tasks.” Artificial Intelligence, 173(5–6), 503–535.
  • Haslum, P., Lipovetzky, N., Magazzeni, D., & Muise, C. (2019). An Introduction to the Planning Domain Definition Language. Morgan & Claypool Publishers.