항 재작성(term rewriting)의 개념을 Wolfram Language/Mathematica의 규칙, 패턴, 평가 순서, 가정(assumptions)과 함께 살펴보고, 대수 단순화와 특수함수·적분 같은 상징 계산이 어떻게 재작성 시스템으로 구현되는지 설명한다.
지난주 연재에 이어, 이번에는 항 재작성(term rewriting)이라는 주제를 다룬다. 항 재작성은 변환(규칙이라고 부름)을 기술하는 프로그래밍적 시스템으로 이루어진 매우 일반적인 계산 모델이며, 이 규칙들이 항(term)이라 불리는 표현식을 다른 항들의 집합으로 변환한다.
가장 널리 쓰이는 재작성 엔진들은 흔히 로직 프로그래밍, 증명 보조기(proof assistant), 컴퓨터 대수 시스템에서 사용되는 프로그램과 언어의 핵심에 자리한다. 그중 가장 유명한 것 중 하나가 Mathematica와 Wolfram language다. 이는 Wolfram Research가 과학 계산 프레임워크의 일부로 제공하는 독점 프로그래밍 언어다. 이 시스템의 핵심에는 수학적 표현을 나타내는 복합 기호 표현식을 조작할 수 있는 재작성 시스템이 있다. Maude, Pure, Aldor, 일부 Lisp 변종 같은 다른 언어들도 유사한 시스템을 구현하지만, 여기서는 일반 개념을 설명하기 위해 Mathematica로 작성한 코드를 사용한다.
Mathematica는 보통 노트북 환경에서 실행되며, In과 Out 표현식은 REPL에서 입력한 각 줄마다 단조 증가하는 인덱스로 색인된 벡터다.
Wolfram Language 12.0.1 Engine for Linux x86 (64-bit)
Copyright 1988-2019 Wolfram Research, Inc.
In[1]:= 1+2
Out[1]= 3
In[2]:= 1+2+x
Out[2]= 3 + x
In[3]:= List[x,y,z]
Out[3]= {x, y, z}
이 언어는 본질적으로 표현식(expression)을 다루는 Lisp에 가깝고, 표현식에는 위의 x 항처럼 기호 항(symbolic term)이 포함될 수 있다. 이런 표현식들은 변수가 아니라, 표현식 안에서 변수를 나타내는 기약(더 이상 줄일 수 없는) 원자다. 복합 표현식은 Lisp의 S-표현식과 비슷하며, 머리(head) 항과, 그 표현식의 인수(arguments)가 되는 중첩된 하위 표현식들의 집합으로 구성된다.
F[x,y]
이 경우 F가 머리이고 x와 y가 인수다. 이런 표기 형식은 M-표현식(M-expression)이라 부른다. 핵심 표기는 언어 구성 요소가 모두 기호 표현식이며, 규칙에 의해 조사(introspect)되고 변환될 수 있다는 점이다. 예를 들어 Head 함수는 주어진 표현식에서 머리 기호를 추출한다.
In[4]:= Head[f[a,b,c]]
Out[4]= f
In[5]:= Symbol["x"]
Out[5]= x
In[6]:= Head[x]
Out[6]= Symbol
주어진 M-표현식의 인수들은 Level 함수를 이용해 추출할 수 있는데, Level은 특정 깊이의 인수들을 벡터(중괄호로 표기)로 뽑는다. 여기서는 첫 번째 레벨이 인수 a, b, c다.
In[7]:= Level[f[a,b,c],1]
Out[7]= {a, b, c}
표현식은 여러 형태로 작성할 수 있으며, 결국 이 기본 M-표현식 형태로 환원된다. 예를 들어 덧셈 연산은 Plus 머리를 가진 표현식의 문법 설탕(syntactic sugar)에 불과하다. FullForm 함수를 사용하면 이 표현식을 내부의 정규(canonical) 형태로 줄일 수 있다. 곱셈 역시 중위(infix) 표기로는, 일반적인 대수 관례처럼 각 항을 공백으로 구분해 나타낸다.
In[8]:= FullForm[x+y]
Out[8]//FullForm= Plus[x, y]
In[9]:= FullForm[x y]
Out[9]//FullForm= Times[x, y]
중위 문법 설탕 외에도, 연산자 @와 //를 사용하면 함수를 인수에 각각 전위(prefix) 또는 후위(postfix) 형태로 적용할 수 있다.
In[10]:= Sin[x] (* Full form *)
Out[10]= Sin[x]
In[11]:= Sin @ x (* Prefix sugar *)
Out[11]= Sin[x]
In[12]:= x // Sin (* Postfix sugar *)
Out[12]= Sin[x]
복잡한 수학 표현식은 항들의 중첩 조합일 뿐이다. 예를 들어 간단한 단항식 표현
는 다음과 같이 주어진다.
In[13]:= FullForm[x^3 + (1 + x)^2]
Out[13]//FullForm= Plus[Power[x, 3], Power[Plus[1, x], 2]]
In[14]:= TeXForm[x^3 + (1 + x)^2]
Out[14]//TeXForm= x^3+(x+1)^2
이 표현식 자체는 그래프 구조이며, 구현은 하위 표현식들을 가리키는 포인터를 가진 노드들의 집합으로 이루어진다. 대괄호를 이용한 인덱스 표기는 특정 하위 표현식을 직접 조작하는 데 쓰이며, 머리 항부터 시작해 왼쪽에서 오른쪽으로 열거된다.
In[15]:= f[a,b,c][[0]]
Out[15]= f
In[16]:= f[a,b,c][[1]]
Out[16]= a
In[17]:= f[a,b,c][[2]]
Out[17]= b
표현식의 개별 인수는 인덱스로 슬롯을 참조해 재정렬하거나 다른 표현식에 대입할 수 있다.
In[18]:= F[#3, #1, #2] & [x, y, z]
Out[18]= F[z, x, y]
복잡한 수학 표현식은 표현식 그래프 형태로 나타낼 수 있고, 그래픽 트리 형태로 렌더링할 수 있다. 사실상 이 시스템의 모든 규칙과 함수는 유향 그래프를 다른 유향 그래프 구조로 변환하는 작업이다. 예를 들어 간단한 삼각함수 급수는 기호적으로 다음과 같이 표현할 수 있다.
In[19]:= Series[Cos[x]/x, {x, 0, 10}]
이는 내부적으로 다음과 같은 M-표현식 그래프 구조로 표현된다.
In[20]:= FullForm[Series[Cos[x]/x, {x, 0, 10}]]
Out[20]//FullForm= SeriesData[x, 0, {1, 0, Rational[-1, 2], 0, Rational[1, 24], 0, Rational[-1, 720], 0, Rational[1, 40320], 0, Rational[-1, 3628800], 0, Rational[1, 39916800]}, 0, 11, 1]
이 기호 표현식은 Series 항을 평가하여 개별 항들로 확장할 수 있다.
∑x=0 10 cosx x=1 x−x 2+x 3 24−x 5 720+x 7 40320−x 9 3628800+O(x 11)
이 언어에서 평가는 더 이상 적용할 규칙이 없을 때까지 항을 축약(reduction)하는 방식으로 진행된다. 이러한 표현식은 정규형(normal form)에 있다고 말한다. 이 평가 방식은 메모리에 대한 순차 업데이트와 부수효과가 있는 문장들의 순서가 실행 방식인 순차적 문장 기반 언어와는 다르다.
예를 들어 Range 함수는 리스트 형태로 값들의 열을 만든다. 이 리스트는 각 원소에 함수를 적용하는 다른 함수로 넘길 수 있는데, 예컨대 주어진 정수가 소수인지 질의하는 함수를 적용할 수 있다.
In[20]:= Range[1,10]
Out[20]= {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}
In[21]:= Map[PrimeQ, Range[1,10]]
Out[21]= {False, True, True, False, True, False, True, False, False, False}
이 불리언 열이 최종 형태이며, 현재 스코프에서 이후에 적용할 수 있는 규칙이 없으므로 최종 표현식이 반환된다.
환경에 새로운 사용자 정의 로직을 도입하는 주요 메커니즘은 재작성 규칙의 도입이다. 이는 Rule 정의 또는 그 중위 문법 설탕인 ->로 정의한다. 좌변은 패턴 문법으로 주어지며, 우변에 대해 변수 바인딩을 수행할 수 있다.
예를 들어 정수 1이 등장하는 모든 위치를 2로 쓰는 규칙은 다음과 같다.
In[22]:= Rule[1,2]
Out[22]= 1 -> 2
또는 기호 x의 명시적 출현을 모두 기호 y로 바꾸는 규칙은 다음과 같다.
In[23]:= Rule[x,y]
Out[23]= x -> y
부분 표현식과 매치하고 이름을 규칙의 스코프에 바인딩하는 패턴 변수도 도입할 수 있다. 이 “구멍(hole)”에 대한 매치 결과는 우변에서 변수 이름으로 바인딩된다. 예를 들어 임의의 수량 x_를 매치하고 이를 정의 x에 바인딩하는 규칙은 다음과 같다.
In[24]:= Rule[x_,x]
Out[24]= x_ -> x
더 유용하게는 이러한 패턴 변수가 표현식 내부에 나타날 수 있다. 예를 들어 sin 함수에 주어진 어떤 인수든 cos 함수로 재작성하고 싶다면, 다음 규칙을 쓸 수 있다.
In[25]:= Sin[x_] -> Cos[x]
Out[25]= Sin[x_] -> Cos[x]
규칙은 ReplaceAll 함수 또는 중위 형태 /.를 사용해 주어진 표현식에 적용할 수 있다. 이는 왼쪽의 표현식에 규칙을 적용한다.
In[26]:= ReplaceAll[x, Rule[x,y]]
Out[26]= y
In[27]:= x /. Rule[x,y]
Out[27]= y
위의 삼각함수 예시에서는, 중첩된 삼각함수들을 표현식 본문 안에서 재작성할 수 있다.
In[28]:= Sin[a+b] /. Sin[x_] -> Cos[x]
Out[28]= Cos[a + b]
ReplaceAll에 규칙 리스트를 인수로 넘기면 규칙들을 결합할 수 있다. 예를 들어 다음은 주어진 리스트에 대해 한 번 패스하며 x를 y로, y를 z로 재작성한다.
In[29]:= {x,y,z} /. {x->y, y->z}
Out[29]= {y, z, z}
규칙이 순서대로 적용되며, 마지막 규칙에는 중간 표현식이 입력으로 들어가기 때문에 전체 리스트가 동일한 원소로 변환되지는 않는다. 하지만 ReplaceRepeated는 고정점(fix point)에 도달할 때까지, 즉 마지막 축약 결과와 항이 동일해질 때까지 주어진 규칙 집합을 반복 적용한다.
In[30]:= ReplaceRepeated[x, Rule[x,y]]
Out[30]= y
In[31]:= ReplaceRepeated[x, {Rule[x,y], Rule[y,z]}]
Out[31]= z
In[32]:= {x,y,z} /. {x->y, y->z} (* Non-repeated *)
Out[32]= {y, z, z}
In[33]:= {x,y,z} //. {x->y, y->z} (* Repeated *)
Out[33]= {z, z, z}
이 과정이 무한히 반복되어 수렴하지 않는 규칙 집합을 정의하는 것도 충분히 가능하다. 이 경우 정규형이 없고, 시간(또는 공간)이 폭발하거나 런타임이 포기할 때까지 계속된다.
In[34]:= {1,2} //. {1 -> 2, 2 -> 1}
ReplaceRepeated::rrlim: Exiting after {1, 2} scanned 65536 times.
많은 규칙 집합은 여러 재작성 경로를 허용하며, 그 경로들이 반드시 같은 최종 항으로 이어지지는 않는다. 재작성 순서를 어떻게 고르든 최종 결과가 변하지 않는 규칙 시스템을 합류적(confluent)이라고 한다. 런타임 내부의 재작성 규칙에 사용되는 평가 순서에 대한 처방은 임의적 선택이지만, Mathematica는 표현식의 머리를 평가한 다음 각 요소를 평가한다. 이 요소들 또한 표현식이므로 동일한 평가 절차가 재귀적으로 적용된다.
표준 라이브러리에는 대수적 단순화와 항 재정렬을 위한 이런 변환 집합이 많이 들어 있다. FullSimplify 함수가 가장 일반적이며, 내부에 정의된 방대한 항등식과 관계의 코퍼스를 기반으로 실수값 대수 표현식을 수집하고 단순화한다.
In[35]:= FullSimplify[x^2 x + y x + z + x y]
Out[35]= Plus[Power[x, 3], Times[2, x, y], z]
하지만 이런 규칙 집합은 우리가 직접 도입하고 확장할 수도 있다. 예를 들어 주어진 항등식에 따라 삼각함수를 단순화하는 새로운 간단한 규칙 집합을 인코딩하고 싶다면, 다음 수학 항등식에 대한 규칙을 쓸 수 있다.
sin(α+β)=sinα cosβ+cosα sinβ
cos(α+β)=cosα cosβ−sinα sinβ
이는 다음 두 개의 패턴과 재작성으로 인코딩된다.
In[36]:= ElemTrigExpand = {
Sin[a_ + b_] -> Sin[a] Cos[b] + Cos[a] Sin[b],
Cos[a_ + b_] -> Cos[a] Cos[b] - Sin[a] Sin[b]
}
그다음 선형 인수를 갖는 삼각함수들에 이 규칙을 반복 적용해, 중첩된 항들을 단일 변수 형태로 줄일 수 있다.
In[37]:= Sin[a+b+c] //. ElemTrigExpand
Out[37]= Cos[a] (Cos[c] Sin[b] + Cos[b] Sin[c]) Sin[a] (Cos[b] Cos[c] + Sin[b] Sin[c])
규칙 안에 나타나는 항들은 규칙이 분기(dispatch)할 수 있는 추가 구조를 가질 수 있다. 기호는 Attributes를 정의할 수 있는데, 이는 축약과 기호들의 정규형 재정렬에 영향을 준다. 흔히 결합법칙(associativity), 교환법칙(commutativity), 항등원(identities), 영원(annihilation) 같은 공통 대수 성질이다.
In[38]:= Attributes[f] = {Flat, OneIdentity}
Out[38]= {Flat, OneIdentity}
In[39]:= f[1, f[2, f[3, 4]]] (* Associative *)
Out[39]= f[1, 2, 3, 4]
In[40]:= f[f[1]] (* Idempotent *)
Out[40]= f[1]
함수의 구조적 성질 외에도, 기호는 그 기원과 정의된 영역 또는 집합에 대한 가정으로 풍부해질 수 있다. 예를 들어 어떤 수가 0이 아닌지, 정수인지, 소수인지, 또는 어떤 집합의 원소인지 같은 것들이다. 이런 성질들 자체도 기호 표현식이다. 예컨대 변수 z가 복소평면에 속한다는 가정을 인코딩하려면:
z∈C
Complexes가 C를 나타내는 내장(builtin)이라고 할 때, 다음과 같은 표현식을 쓸 수 있다.
이들은 Assumptions 변수로 정의되는 전역 가정 집합에 추가할 수 있다.
In[42]:= $Assumptions = {a > 0, b > 1}
Out[42]= a > 0
이런 대수적 단순화를 위한 재작성은, redex(축약 가능한 부분식)에서 마주치는 항의 가정에 따라 분기하고, 기호의 성질에 대한 연역 사슬을 바탕으로 서로 다른 축약 경로를 선택한다. 예를 들어 제곱의 제곱근이 항등으로 줄어드는 항등식은 주어진 기호의 부호에 의존한다. Refine 함수를 사용하면 전역 가정을 포함시켜 단순화기가 어떤 분기를 선택해야 하는지 알려줄 수 있다.
In[43]:= Refine[Sqrt[a^2 b^2]]
Out[43]= a b
기호에 대한 술어의 진릿값도 이 함수로 질의할 수 있다. 이는 True, False 또는 해당 기호에 지역 가정이 없을 때의 부정결(indeterminate) 답을 반환한다.
In[44]:= Refine[Positive[b]]
Out[44]= True
In[45]:= Refine[Positive[x]]
Out[45]= Positive[x] (* Has no truth value *)
많은 함수는 이름 붙은 Assumptions 매개변수도 받는데, 이는 함수에 주어진 인수들에 대해 지역 가정을 도입하는 데 사용할 수 있다.
In[46]:= Refine[Sqrt[x^2], Assumptions -> {x < 0}]
Out[46]= -x
가정 시스템은 제한된 1차 해결(first order resolution)을 수행해, 특정 영역 내에서 기호들의 성질을 추론할 수 있다. 예를 들어 가정 x > 1은 x가 0이 아니고 음수가 아니라는 사실을 함의한다. 또는 정수 y에 대해 y > 2이고 소수라는 가정은 y가 짝수가 아니라는 사실을 함의한다.
규칙 좌변의 패턴은 표현식의 타입뿐 아니라 패턴 변수의 가정과 속성에 대해서도 분기할 수 있다. 예를 들어 좌변 x_Symbol은 어떤 기호적 수량(숫자는 제외)을 매치하고 이를 특정 상수로 재작성할 수 있다. 이 패턴은 List 자체의 머리에 매치하여 머리를 상수로 재작성한다는 점에 유의하라.
In[47]:= {1, x, Pi} /. x_Symbol -> 0 (* Matches List, x, Pi *)
Out[47]= 0[1, 0, 0]
술어 함수는 패턴 변수에 _?s 접미사와 함수로 감싸서 사용할 수 있다. 예를 들어 어떤 항이 수치적 수량인지 확인하려면 NumericQ 함수를 사용할 수 있다. 이는 Pi와 1 항에는 매치하지만 List나 x에는 매치하지 않는다.
In[48]:= {1, x, Pi} /. x_?NumericQ -> 0 (* Matches 1, Pi *)
Out[48]= {0, x, 0}
표준 라이브러리에는 기호적 수량에 대한 가정과 규칙 라이브러리로 인코딩된 방대한 수학 지식 코퍼스가 들어 있다. 예를 들어 리만 제타 함수는 다른 함수들로 나타내는 수백 가지의 알려진 항등식과 표현을 갖는다. 짝수 정수 값에 대해서는 π와 베르누이 수로 표현되는 간단한 닫힌형(closed form)이 있다.
ζ(2)=π 2 6
Mathematica는 이런 항등식을 알고 있으며, Zeta 함수를 이 축약 형태로 자동 변환하도록 선택한다. 짝수가 아닌 값들에 대해서는 (일반적으로) 간단한 닫힌형이 없지만, N 함수를 사용해 임의의 자릿수로 계산 가능한 급수 근사가 존재한다.
In[49]:= Zeta[2]
Out[49]= Times[Rational[1, 6], Power[Pi, 2]]
In[50]:= Zeta[3]
Out[50]= Zeta[3]
In[51]:= N[Zeta[3], 30]
Out[51]= 1.20205690315959428539973816151
유명한 XKCD 만화는 특정 미적분 문제의 비대칭성을 보여준다. 이런 만화는 이 재작성 시스템 안에서 도함수와 적분에 대한 단순화를 인코딩하려 할 때 그대로 드러난다.
실제로 미분은 위의 기법을 사용하면 거의 자명하게 인코딩할 수 있다. 미분 연산자의 선형성, 곱의 미분법, 거듭제곱 미분법, 상수 규칙은 네 줄의 규칙으로 쓸 수 있다. 표준 라이브러리에는 더 큰 코퍼스의 정의가 있지만, 보통 이 정도로 간결하다.
{
Diff[f_ g_, x_] -> f Diff[g, x] + g Diff[f, x],
Diff[f_ + g_, x_] -> Diff[f, x] + Diff[g, x],
Diff[Pow[x_,n_Integer], x_] -> n * Pow[x,n-1],
Diff[x_, x_] -> 1
Diff[n_?NumericQ, x_] -> 0
}
하지만 많은 컴퓨터 대수 시스템은 거의 마법 같은 방식으로 부정적분 계산을 수행할 수 있다. 예를 들어:
In[52]:= Integrate[Log[1/x], x]
Out[52]= Plus[x, Times[x, Log[Power[x, -1]]]]
Mathematica의 기호 적분 능력이 마법처럼 보일 수 있지만, 실제로는 재작성 기계장치에 변환 코퍼스와 1930년대의 몇 가지 해석 결과가 결합된 대표적 사례일 뿐이다. 어떤 적분들은 패턴 매칭으로 직접 계산 가능하지만, Meijer G-function 연구에는 다양한 종류의 초월함수를 적분 계산에 편리한 닫힌형으로 변환할 수 있게 해주는 비자명한 결과가 있다.
Meijer G-function은 4개의 벡터 매개변수로 색인된 함수이며, 다음의 복소 적분으로 표현된다. 여기서 L
은 −i∞에서 i∞까지 달린다.
G m,n p,q(z∣∣a 1,…,a n,a n+1,…,a p∣∣b 1,…,b m,b m+1,…,b q)=1 2 π i∫L∏j=1 m Γ(b j−s)∏j=1 n Γ(1−a j+s)∏j=m+1 q Γ(1−b j+s)∏j=n+1 p Γ(a j−s)z s d s
이는 잘 연구된 함수이며, 놀랍게도 매우 많은 종류의 특수함수(삼각함수, 베셀 함수, 초등기하급수함수(hypergeoemtric) 등)가 G 함수로 표현될 수 있다. 따라서 우리는 복잡하게 중첩된 함수들을 G-함수 항을 조작하는 것만으로 줄일 수 있다. 이렇게 줄인 표현식에 적분 정리를 적용하면 하나 이상의 다른 G-함수 항이 나오고, 그 결과를 다시 특수함수로 전개하여 적분 결과를 얻는다. 이 방법이 보편적으로 통하는 것은 아니지만, 실용적으로는 충분히 많은 경우에 적용되어 매우 유용하다.
아주 일반적인 부정적분 정리 중 하나는 피적분함수를 G-함수 인덱스의 순열(permutation)로 재표현한다. 좌변에는 적분 표현식이 있고 우변에는 G-함수로 계산된 적분이 있다.
∫G m,n p,q(z∣∣a 1,…,a n,a n+1,…,a p∣∣b 1,…,b m,b m+1,…,b q)d z=G m,n p+1,q+1(z∣∣1,a 1+1,…,a n+1,a n+1+1,…,a p+1∣∣b 1+1,…,b m+1,0,b m+1+1,…,b q+1)
적분 전체 책 한 권이, 몇 줄의 항 재작성 로직으로 된 G-함수의 곱셈 및 변환 규칙 집합으로 환원될 수 있다.
Mathematica의 적분 엔진 핵심에는 이런 접근을 포함한 변환들과, 꽤 잘 작동하는 다양한 다른 휴리스틱이 있다. 예를 들어 MeijerGReduce 함수는 많은 종류의 특수함수를 G-함수 등가물로 변환할 수 있으며, 그다음 FullSimplify와 다른 항등식들이 이 표현식들을 더 줄일 수 있다.
In[53]:= MeijerGReduce[Sqrt[x] Sqrt[1+x],x]
x 1+x⇒−x G 0,0 1,1(x|3 2,0−)2 π
이 모든 기능의 합류는, 대부분의 주류 언어의 의미론과는 크게 다른 방식으로 추상 표현식을 다루고 작업하도록 맞춰진 프로그래밍 환경을 만들어낸다.
이 시스템으로 임의의 로직을 프로그램할 수 있는 것은 사실이지만, 제자리 참조(in-place reference)와 가변 데이터 구조를 다루는 명령형 로직을 코딩하려 하면 다소 투박해질 수 있다. 그럼에도 과학 계산에서 강력한 도메인 도구이며, 언어에 드러난 기술 도메인 관련 함수들의 수는 수십 년에 걸친 세심한 전문가 도메인 지식의 결과다.
많은 대학이 이 소프트웨어에 대한 사이트 라이선스를 가지고 있으니, 이질적인 평가 모델과 의미론을 가진 프로그래밍 언어에 관심이 있다면 이 시스템에서 찾을 수 있는 아이디어를 직접 만져보는 것도 가치가 있다.