10374번 - Combinator Expression 다국어

Combinatory logic may be thought as one of computational models allowing to express any computable function as a composition of functions from a small finite basis. In this problem we consider a restricted variant of BCKW basis, BCKI.

Combinator expression in BCKI basis is a string, corresponding to the following grammar:

⟨Expression⟩ ::= ⟨Expression⟩ ⟨Term⟩ | ⟨Term⟩
⟨Term⟩ ::= ‘(’⟨Expression⟩‘)’ | ‘B’ | ‘C’ | ‘K’ | ‘I’

As we can see from the grammar, the expression is a tree of applications where leafs are combinators \(B\), \(C\), \(K\) and \(I\). The application is left-associative. For example \(BIC\) is equivalent to \((BI)C\), but not to \(B(IC)\).

For the sake of the explanation we will use lowercase English letters (a ... z) to represent sub-expressions. These lowercase letters will not appear in real data. For example, \(BIC\) can be represented by \(BxC\) (that is, \(B\underbrace { I }_{ x }C\)), \(x\) (\(\underbrace { BIC }_{ x }\)), \(xy\) (\(\underbrace { BI }_{ x } \underbrace { C }_{ y }\)), \(Bxy\) (\(B\underbrace { I }_{ x }\underbrace { C }_{ y }\)), but not by \(Bx\).

We say that in expression \(pq\) we apply \(p\) to \(q\). We can employ our intuition by saying that \(p\) is a function and \(q\) is its parameter. However, the evaluation process is quite different from traditional computation — instead of passing values over fixed expression tree, we evaluate by altering that tree so that the result is also some combinator expression.

To evaluate an expression, we need to select some sub-expression, corresponding to one of the patterns specified in the table below — that is, there should exist such \(x\) (and maybe \(y\) and \(z\)) that the pattern from the table becomes equal to the sub-expression. Then we need to replace the sub-expression with the reduction result from the table.

After the replacement took place we must repeat the process, until there remains no suitable subexpressions. This final expression is normal form of the original one. For example, in expression \(CIC(CB)I\) we can make the following letter assignment

\[\underbrace { C }_{ C }\underbrace { I }_{ x }\underbrace { C }_{ y }\underbrace { (CB) }_{ z }I\]

and see that \(CIC(CB)I\) ≡ \((((CI)C)(CB))I\) ≡ \((((Cx)y)z)I\) contains \(C\) combinator pattern and thus reduces to \(((xz)y)I\) ≡ \(I(CB)CI\):

\[(\underbrace { C }_{ C }\underbrace { I }_{ x }\underbrace { C }_{ y }\underbrace { (CB) }_{ Z })I \rightarrow (\underbrace { I }_{ x } \underbrace { (CB) }_{ z }\underbrace { C }_{ y })I\]

One more example: \(B((CK)I)IC\) expression. Let us first reduce combinator \(B\):

\[(\underbrace { B }_{ B }\underbrace { ((CK)I) }_{ x }\underbrace { I }_{ y }\underbrace { C }_{ z } \rightarrow \underbrace { ((CK)I) }_{ x } (\underbrace { I }_{ y }\underbrace { C }_{ z })\]

Now, let’s reduce the last \(I\):

\[((CK)I)(\underbrace { I }_{ I } \underbrace { C }_{ x }) \rightarrow ((CK)I)C\]

And now we finish evaluation with two more reductions:

\[((\underbrace { C }_{ C }\underbrace { K }_{ x }) \underbrace { I }_{ y }) \underbrace { C }_{ z } \rightarrow (\underbrace { K }_{ K }\underbrace { C }_{ x }) \underbrace { I }_{ y } \rightarrow C\]

It is possible to show that the normal form remains the same irrespectable to the order of evaluation. For example, the following evaluation order:

\[C(K(II)(\underbrace { I }_{ I }\underbrace { C }_{ x })) \rightarrow C(K(\underbrace { I }_{ I }\underbrace {  I}_{ x })(C)) \rightarrow C((\underbrace { K }_{ K }\underbrace { I }_{ x }) \underbrace { C }_{ y }) \rightarrow CI\]

leads to the same result as 

\[ C(K(\underbrace {I  }_{ I }\underbrace { I }_{ x })(IC)) \rightarrow C((\underbrace { K }_{ K }\underbrace { I }_{ x })\underbrace { (IC) }_{ y }) \rightarrow CI\]

However, as you see, the number of reductions is different: 3 in the first case and 2 in the second. This poses an interesting problem — to find an evaluation order with the minimal number of reductions for a given formula.

Your task is to write a program which finds the minimal number of reductions required for a given combinator expression to be evaluated to its normal form.

The only line of the input file contains a combinator expression corresponding to the grammar above. The length of the expression does not exceed 30 000. The expression contains no whitespaces or symbols not specified in the grammar.

Output a single integer — the minimal number of reductions required for the given formula to evaluate it to normal form.