콤비네이터 식

문제

조합 논리는 계산 가능한 모든 함수를 작은 기본 집합에 속한 함수의 합성으로 나타내는 계산 모형이다. 이 문제에서는 BCKW 기저를 제한한 BCKI 기저를 다룬다.

BCKI 기저의 콤비네이터 식은 다음 문법이 만들어 내는 문자열이다.

<식> ::= <식> <항> | <항>
<항> ::= '(' <식> ')' | 'B' | 'C' | 'K' | 'I'

문법에서 보듯 식은 적용을 내부 노드로 삼고 콤비네이터 $B$ , $C$ , $K$ , $I$ 를 잎으로 삼는 트리다. 적용은 왼쪽 결합이므로 $BIC$ 는 $(BI)C$ 와 같고 $B(IC)$ 와는 다르다.

아래 설명에서 알파벳 소문자 a부터 z까지는 부분식을 나타낸다. 이 소문자는 실제 입력에 나오지 않는다. 예를 들어 $BIC$ 는 $BxC$ ( $x = I$ ), $x$ ( $x = BIC$ ), $xy$ ( $x = BI$ , $y = C$ ), $Bxy$ ( $x = I$ , $y = C$ ) 꼴에 들어맞지만 $Bx$ 꼴에는 들어맞지 않는다.

식 $pq$ 에서는 $p$ 를 $q$ 에 적용한다고 말한다. $p$ 를 함수로, $q$ 를 인자로 읽어도 좋다. 다만 계산 방식은 값을 고정된 트리에 흘려보내는 방식이 아니다. 한 단계마다 트리 자체를 고쳐 쓰고, 그 결과도 다시 콤비네이터 식이다.

한 단계는 아래 표의 패턴 가운데 하나와 같아지는 부분식을 고른다. 즉 패턴이 그 부분식과 똑같아지도록 부분식 $x$ 를(필요하면 $y$ 와 $z$ 까지) 잡을 수 있어야 한다. 그런 다음 고른 부분식을 표의 결과로 바꾼다.

패턴	바뀐 결과	이름
$Bxyz$	$x(yz)$	합성 함수
$Cxyz$	$(xz)y$	교환 함수
$Kxy$	$x$	상수 함수
$Ix$	$x$	항등 함수

어떤 패턴에도 맞는 부분식이 없을 때까지 이 과정을 되풀이한다. 마지막에 남은 식이 원래 식의 정규형이다.

$CIC(CB)I$ 를 보자. 이 식은 $(((CI)C)(CB))I$ 로 읽힌다. $x = I$ , $y = C$ , $z = CB$ 로 잡으면 부분식 $(((CI)C)(CB))$ 가 $Cxyz$ 와 같으므로 $(xz)y = I(CB)C$ 로 바뀌고, 식 전체는 $I(CB)CI$ 가 된다.

$B((CK)I)IC$ 도 보자. $x = (CK)I$ , $y = I$ , $z = C$ 로 $B$ 를 줄이면 $((CK)I)(IC)$ 가 된다. 안쪽 $I$ 를 줄이면 $((CK)I)C$ , $C$ 를 줄이면 $(KC)I$ , 마지막으로 $K$ 를 줄이면 $C$ 만 남는다.

정규형은 계산 순서와 상관없이 같지만 단계 수는 순서에 따라 달라진다. $C(K(II)(IC))$ 에서 안쪽 $IC$ 를 먼저 줄이면 $C(K(II)C)$ , 이어서 $II$ 를 줄이면 $C((KI)C)$ , 마지막으로 $K$ 를 줄이면 $CI$ 가 되어 세 단계가 걸린다. 반대로 $II$ 를 먼저 줄이면 $C((KI)(IC))$ 가 되고, $K$ 가 $(IC)$ 를 버리므로 두 단계 만에 $CI$ 에 이른다.

주어진 콤비네이터 식을 정규형까지 계산하는 데 필요한 최소 단계 수를 구하는 프로그램을 작성하라.

입력

첫째 줄에 위 문법을 따르는 콤비네이터 식이 주어진다. 식의 길이는 30000 이하이다. 식에는 공백이나 문법에 없는 문자가 들어 있지 않다.

출력

주어진 식을 정규형까지 계산하는 데 필요한 최소 단계 수를 정수 하나로 출력한다.