연산자 더 알아보기

앞 절들보다 그리 복잡하지는 않지만, 이 내용을 두기엔 여기가 가장 알맞다. 자, 이제 우리는 동시적(concurrent) 알고리즘을 모델링할 수 있고 복잡한 라이브니스 속성(liveness property)도 작성할 수 있다. 그런데 우리가 못 하는 게 뭔지 아는가?

시퀀스(sequence)의 합 구하기다.

뭐, 물론 그 일을 하는 PlusCal 알고리즘이야 작성할 수 있다:

---- MODULE sum ----
EXTENDS Integers, Sequences, TLC, FiniteSets
CONSTANT S
ASSUME S \subseteq Int

SumSeq(s) == 0 \* ???

(*--algorithm dup
variable 
  seq \in [1..5 -> S];
  sum = 0;
  i = 1;

define
  TypeInvariant ==
    /\ sum \in Int
    /\ i \in 1..Len(seq)+1

  IsCorrect == pc = "Done" => sum = SumSeq(seq)
end define; 

macro add(x, val) begin
  x := x + val
end macro;

begin
  Iterate:
    while i <= Len(seq) do
      add(sum, seq[i]);
      add(i, 1);
    end while;
end algorithm; *)
====

spec

그런데 SumSeq는 대체 어떻게 작성한단 말인가?!

지금까지 배운 것만으로도 이걸 할 수는 있지만, 정말 복잡하고 짜증 나는 일이라 여러분이 혼자서 알아내리라고는 기대하지 않는다. 나중에 주제별 심화 글 같은 걸로 빼 둘지도 모르겠다. 하지만 바로 이 시퀀스 합산의 짜증스러움이 계기가 되어, 2008년 TLA+에 재귀 연산자(recursive operator)가 추가되었다.

재귀 연산자

재귀 연산자는 다음처럼 미리 선언해 두어야 한다:

RECURSIVE SumSeq(_)

(_)는 연산자가 받을 인자의 개수를 미리 밝혀 두는 것이다. 그러니 매개변수가 2개인 연산자라면 Op(_, _)라고 쓴다. 이렇게 해 두면 연산자를 평소처럼 정의하면 되는데, 다만 자기 자신을 참조할 수 있다는 점이 다르다:

SumSeq(s) == IF s = <<>> THEN 0 ELSE
  Head(s) + SumSeq(Tail(s))

쉽다. 사실 RECURSIVE 부분을 LET 안에 넣어서 헬퍼 연산자를 만들 수도 있다:

SumSeq(s) == LET
  RECURSIVE Helper(_)
  Helper(s_) == IF s_ = <<>> THEN 0 ELSE
  Head(s_) + Helper(Tail(s_))
IN Helper(s)

재귀가 끝나는지를 문법 차원에서 검사해 주지는 않는다. 끝없이 도는 재귀가 있으면 TLC가 스택 오버플로 에러를 던진다.

집합에 대한 재귀와 교환법칙

집합(set)의 합을 구할 때도 같은 방식을 쓰려면, 재귀를 위해 원소 하나를 골라낼 방법이 필요하다. 당연히 가장 쉬운 방법은 CHOOSE를 쓰는 것이다.

RECURSIVE SetSum(_)

SetSum(set) == IF set = {} THEN 0 ELSE
  LET x == CHOOSE x \in set: TRUE
    IN x + SetSum(set \ {x})

이걸 보면 걱정이 들어야 한다. 고를 수 있는 x가 하나로 정해지지 않는다: 집합의 모든 원소가 TRUE를 만족한다! 이는 곧 TLC가 가장 작은 값을 고른다는 뜻이다.

RECURSIVE SetToSeq(_)

SetToSeq(set) == IF set = {} THEN <<>> ELSE
  LET x == CHOOSE x \in set: TRUE
    IN <<x>> \o SetToSeq(set \ {x})

>>> SetToSeq({6, 8, 1, 2, -1, 5})

<<-1, 1, 2, 5, 6, 8>>

SetSum에서처럼 이게 상관없을 때도 있다. 하지만 상관이 있을 수도 있다면, 최솟값을 명시적으로 고르게 하는 식으로, CHOOSE에 원소 하나만 만족하는 선택 술어(predicate)를 지정해야 한다.

고차 연산자

다음은 다른 연산자를 함수처럼 인자로 받는 연산자다. 이런 게 있으면 SeqMap을 만들 수 있다. 함수(function)를 써서 SeqMap을 정의하면 이렇다:

SeqMap(f, seq) == [i \in DOMAIN seq |-> f[seq[i]]]

하지만 연산자를 쓰고 싶다면 대신 이렇게 쓴다:

SeqMap(Op(_), seq) == [i \in DOMAIN seq |-> Op([seq[i]])]

그리 나쁘지 않다. LAMBDA로 익명 연산자를 정의할 수도 있다:

SeqMap(LAMBDA x: x + 1, <<1, 2, 3>>)
\* <<2, 3, 4>>

경고

재귀 연산자와 고차 연산자(higher-order operator)는 함께 쓸 수 없다.

이항 연산자

Sequences 모듈의 정의를 들여다보면 \o를 어떻게 정의하는지 알 수 있다:

s \o t == [i \in 1..(Len(s) + Len(t)) |-> IF i \leq Len(s) THEN s[i]
                                                         ELSE t[i-Len(s)]]

\o는 이항 연산자(binary operator)다. 직접 정의할 수 있는 이항 연산자는 \o, +, \prec처럼 고정된 목록으로 정해져 있다. 스펙을 헷갈리게 만들기 때문에 나는 대체로 이렇게 하는 걸 좋아하지 않지만, 자주 쓰는 게 두어 개 있다:

set ++ x == set \union {x}
set -- x == set \ {x}

함수 연산자

이건 최상위 함수를 작성할 때 쓰는 약간의 문법 설탕(syntactic sugar)이다:

Double == [x \in 1..10 |-> x * 2]

\* can also be written as

Double[x \in 1..10] == x * 2

주로 재귀 함수를 작성할 때 쓴다:

Factorial[x \in 0..10] == IF x = 0 THEN 1 ELSE x * Factorial[x - 1]

CASE

달리 넣을 데가 없어서, 빠짐없이 다룬다는 차원에서 그냥 여기에 던져 둔다.

Fizzbuzz(x) ==
  CASE (x % 3 = 0) /\ (x % 5 = 0) -> "Fizzbuzz"
    [] (x % 3 = 0)                -> "Fizz"
    [] (x % 5 = 0)                -> "Buzz"
    [] OTHER                      -> x

아무것도 일치하지 않으면(그리고 OTHER도 없었다면) TLC는 에러를 낸다. 둘 이상이 일치하면 실제로 무엇이 실행될지는 구현 정의(implementation-defined)이며, TLC는 일치하는 첫 번째 선택지를 고른다.