[PLT/프로그래밍언어론] 14. Logical Programming(2)

14. logical 2

#PLT

논리 프로그래밍(Logic Programming)

First-order Logic

• 논리 프로그램(Logic Program)은 기본적으로 논리식(Logic Formulae)의 집합이다.
• 따라서 이러한 논리식을 작성하기 위한 언어가 필요하다.
• 여기서 다루는 것은 First-order Logic이며, 이는 predicate logic 또는 predicate calculus으로도 알려져 있다.
• 이는 propositional logic(명제 논리), 0th-order 및 higher-order logic와 구분된다.

Propositional Logic vs Predicate Logic

• Propositional Logic와 달리 first-rder logic는 predicate(술어)와 quantifier(한정자)를 다룬다.
• predicate: 변수와 함께 참/거짓으로 평가되는 논리적 함수.
• Propositional Logic: "인간은 필멸이다."
• First-order Logic: "모든 x에 대해, x가 인간이라면, x는 필멸이다."
  
• 원자식(atom, atomic formula): 더 이상 나눌 수 없는 기본적인 formula.
• Propositional Logic에서 atom는 propositional variable이다.
  • 예: P, Q
• Predicate Logic에서 atom는 대개 predicate symbol와 그 argument로 이루어진다.
  • 예: p(x), q(y, z)
• atomic formula(원자식)은 리터럴(literal)이라고도 한다.
  • positive literal: an atom, p(x)
  • negative literal: the negation of an atom, ¬p(x).

용어(Terminology)

• 일차 논리의 핵심 요소:
  • 알파벳(Alphabet)
  • 항(term)
  • 정형화된 공식(Well-formed Formulae, WFF)

알파벳(Alphabet)

• 알파벳은 기호(symbol)의 집합이다.
• 여기서 알파벳은 두 집합으로 이루어진다.
  • 일차 논리에 공통적인 Logical symbols
    • ¬, ^, v, ->, …
  • 특정 논의 영역(domain of discourse)에 특화된 Non-logical symbols
  • 논의 영역(Domain of Discourse): 한정자(quantifier)가 작용하는 대상의 집합.
    • 예: "모든 x에 대하여, x가 실수라면..."에서 실수들의 집합이 논의영역.

논리 기호(Logical Symbols)

• 논리 연결자(Logical Connectives): ¬ (부정), ∧ (논리곱), ∨ (논리합), ⟶ (함의), ⟷ (동치)
• 명제 상수(Propositional Constants): true, false
• 한정자(Quantifiers): ∃ (존재한다), ∀ (모든)
• 구두점 기호(Punctuation Symbols): '.', ',', '(', ')' 등
• 변수(Variables): X, Y, Z

비논리 기호(Non-logical Symbols)

• 논의영역에 대한 술어(Predicate), 함수(Function), 상수(Constant)
• 비논리 기호는 술어 기호와 함수 기호 집합으로 정의되는 시그니처(signature)에 의해 정의된다.
  • 술어 시그니처(Predicate Signature): n항(n-ary)의 술어 기호 집합.
    • 예: p(X): "X는 학생이다", q(X, Y): "X는 Y보다 작다."
    • 얘는 X를 설명해주고 있다.
  • 함수 시그니처(Function Signature): 항수(arity)를 갖는 함수 기호 집합.
    • 예: f(X): "X의 아버지", g(X, Y): "X+Y"
    • 얘는 X에다가 뭔가를 한 object를 설명한다
  • 0항 함수(0-arity function)는 상수(constant)이며, 보통 a, b, c,... 로 표기.

항(Terms)

• Term의 집합은 다음과 같이 귀납적으로 정의된다.
• 변수(Variable): 모든 변수는 term이다.
• 함수(Function): f(t1, ..., tn)이 term이 되려면, f는 함수 기호이고 t1, ..., tn은 term이다.
  • ex) loves(X, jack)
• 변수가 없는 항을 기저 항(ground term)이라고 한다.
  • ex) loves(jone, jack)

논리식(Formulae)

• 정형 논리식(Well-Formed Formulae, WFF)은 다음과 같이 귀납적으로 정의된다.
  1. t1, t2, ..., tn이 term이고 p가 predicate라면 p(t1, t2, ..., tn)는 formula이다.
  2. true와 false는 formula이다.
  3. F와 G가 formula이라면, ¬F, (F ∧ G), (F ∨ G), (F ⟶ G), (F ⟷ G) 역시 공식이다.
  4. F가 formula이고 x가 variable라면, ∀x.F, ∃x.F도 formula이다.
  
  
  
• formula은 term들에 대한 특성을 나타낼 수 있다.
• 예를 들어 gt(>)라는 predicate가 있을 때, gt(3,2)는 참일 수 있다.
• predicate들은 logical connective와 결합하여 더 복잡한 표현을 형성한다.
• 전이성(transitivity)을 나타내는 formula:
  • gt(X, Y) ∧ gt(Y, Z) ⟶ gt(X, Z)

절(Clauses)

• 절(Clause)은 literal들의 논리합(disjunction)이다.
  • 예: P ∨ ¬Q ∨ R ∨ ¬S
• 이를 implicative form로 나타낼 수도 있다.
  • H1, …, Hm ← A1, …, An

Horn Clause

• Horn Clause: 양의 리터럴이 최대 한 개만 있는 절.
• Definite Clause: 정확히 하나의 양의 리터럴을 가지는 호른 절.
  • H :- A1, ..., An
  • 이는 A1 ∧ A2 ∧ ⋯ ∧ An → H 와 동일한 의미를 가진다.
• 호른 절은 논리 프로그래밍의 기반이며, 프로로그(Prolog)에서는 모든 절이 호른 절이다.

헤드(Head)와 바디(Body)

• H :- A1, ..., An
• :-의 왼쪽은 절의 헤드(Head)
• :-의 오른쪽은 절의 바디(Body)
  • 바디가 없는 호른 절은 사실(Fact)이다.
  • Definite Clause은 규칙(Rule)이다.
  • 쿼리(Query) 또는 목표(Goal)는 헤드 없이 바디만 있는 호른 절이다.

논리 변수(Logic Variable)

• 논리 변수와 변경 가능한 변수(modifiable variable) 사이에는 몇 가지 차이가 있다.
• One-time Binding: 논리 변수는 한 번 특정 term에 결합되면 다른 term으로 결합할 수 없다.
  • 예: X가 a에 결합되었다면, X에 다른 상수 b를 결합할 수 없다.
• Partial Definition: 논리 변수의 값은 부분적으로 정의될 수 있다.
  • 예: X가 f(Y, Z)에 결합된 경우, Y나 Z에 대한 결합이 이루어지면 X의 값도 그에 따라 구체화된다.
  • 만약 modifiable variable X = (a + b) * t - 5이고, 이 값이 7이라면, x = 7이 된다. 즉, 표현식이 제대로 evaluate되야 값이 바뀐다. 그 전에는 결정할 수 없다.
  • 함수형 프로그래밍에서 x = expr이라면 x는 immutable variable이다.
• 양방향 결합(Bidirectional Binding): 결합은 양방향으로 영향을 준다.
  • 예: X가 f(Y)에 결합되어 있고, 이후 f(b)가 X에 결합되면 Y도 b에 결합된다.
  • X = f(Y), X = f(b), Y = b

해결(Resolution)

• 해결(Resolution)은 기존 절들로부터 새로운 절을 도출하는 과정이다.
• 예:
  cold(X) :- snowy(X)
  snowy(Seoul)

  ---

  cold(Seoul)

논리 프로그래밍(Logic Programming)

• 프로그래머는 일련의 axiom(공리)를 제시하고, 여기서 goal이 증명될 수 있다.
• 논리 프로그램 사용자는 goal 또는 query를 제시한다.
• 언어 구현은 주어진 goal를 만족하는 axiom 및 inference step를 찾아 나간다.
  • 변수에 대한 값(해(solution))을 찾는 과정.
• 프로로그(Prolog)에서 이 과정을 경험했지만, 특정 언어에 제한되지는 않는다.

치환과 합일(Substitution and Unification)

치환(Substitution)

• 치환(Substitution): 변수를 term으로 매핑하는 함수.
• 자기 자신과 다르게 매핑되는 변수의 수는 유한하다.
  • 𝒟 = { X1/t1, ..., Xn/tn }
    • Xi (i=1,...,n)은 서로 다른 변수이고, ti는 항이며 Xi와 다르다.
  • Domain(𝒟) = {X1, ..., Xn}, Codomain(𝒟) = {Y | Y는 ti 안의 변수, i = 1~n}
  
  
• 예: 𝒟 = { X/a, Y/f(Z) }
  • X를 a로, Y를 f(Z)로. X와 Y가 D의 substitution이고, codomain은 Z이다.
  • 𝒟를 항 g(X, Y, Z)에 적용: g(X, Y, Z)𝒟 = g(a, f(Z), Z)
  • 모든 치환은 동시에 적용된다.(simultaneous)
  • 𝒟 = { Y/f(X), X/a }를 g(X, Y)에 적용하면 g(a, f(X))가 된다.
    • g(a, f(a))로 해석해서는 안 된다.
    • 치환은 동시에 적용된다.

합성(Composition)

• 두 치환 𝒟, 𝒜의 합성 𝒟𝒜는 다음과 같이 정의된다.
• 𝒟 = {X1/t1, ..., Xn/tn}, 𝒜 = {Y1/s1, ..., Ym/sm}일 때,
• {X1/t1𝒜, ..., Xn/tn𝒜, Y1/s1, ..., Ym/sm}에서
  • Xi = ti𝒜이고 Yi가 {X1, ..., Xn}에 속하는 경우 Xi/ti𝒜제거

• 𝒟, 𝒜에 대한 합성은 표현식 E에 대해 E𝒟𝒜 = (E𝒟)𝒜를 만족한다. 즉, 치환은 결합법칙을 가진다.(associative)
• 예: 𝒟 = { X/f(Y), W/a, Z/X }, 𝒜 = { Y/b, W/b, X/Z }
  • 𝒟𝒜 = { X/f(b), W/a, Y/b }
  • f(Y) = t1이고, t1A를 적용, 즉 f(Y)A를 적용하면 Y대신 b를 써서 f(b)가 된다.
  • W/b의 경우 W가 X1, … Xn에 속한다. W/b는 제거한다.
  • Y/b는 A의 substitution이므로 가져옴
  
  
• 𝒟를 적용한 뒤 𝒜를 적용하는 것과 𝒜를 적용한 뒤 𝒟를 적용하는 것은 같다.
• Z/X 뒤에 X/Z를 적용하면 Z가 Z로 돌아오므로 제거된다.

재명명(Renaming)

• 치환 𝛿가 역치환 𝛿⁻¹이 존재하여 𝛿𝛿⁻¹ = 𝛿⁻¹𝛿 = 𝜀가 되면, 𝛿는 재명명(renaming)이다.
• 예: 𝒟 = {X/Y, Y/X}는 단순히 X와 Y 이름을 교환하므로 재명명이다.
  • 치환은 동시에 이루어짐

• 𝒜={X/Y, Z/Y}는 X와 Z를 rename하지만, X와 Z를 동일하게 만들어버려 이전과 달라진다. 따라서 재명명이 아니다.

여기서 Y를 X와 Z중 뭐로 치환할건지 정할 수 없음. renaming이라 할 수 없다.

Preorder over Substitution

• 치환에 대해 준순서(preorder) ≤를 정의할 수 있다.
• 𝒟 ≤ 𝒜는 𝒟가 𝒜보다 더 일반적(more general)임을 의미하며, 𝒟에 어떤 치환 𝛾를 적용하면 𝒜를 얻을 수 있다면 성립한다.
• 즉, 𝒟 ≤ 𝒜 ⇔ ∃𝛾 s.t. 𝒟𝛾 = 𝒜.
  • 𝒟 ≤ 𝒜 iff. there exists a substitution 𝛾 s.t. 𝒟𝛾 = 𝒜.
• 표현식 e와 e'에 대하여, e and e', e ≤ e', iff. ∃𝒟 e𝒟=e'.
• 또한 preorder로 equivalence를 정의할 수 있다.
  • e = e'는 e ≤ e'와 e' ≤ e를 모두 만족할 때 성립한다.

Syntactic Equality

• '=' 기호로 표현.
• 이는 명령형 언어의 대입(assignment)나 수학에서의 등호와는 다르다.
• 두 항 s, t에 대해 s = t라는 술어를 썼을 때, 이는 모든 기저항(ground term)에 대한 syntatic equality을 의미한다.

Syntactic Equality

• 논리 프로그램에서 X = a를 쓰면, 변수 X를 상수 a에 결합하는 해 {X/a}가 존재한다.
  • 적용하면 a = a가 성립하므로 식이 만족된다.
  
  
• a = X 역시 X = a와 동일한 의미를 가진다.
• 명령형 언어에서 "="는 대입 의미를 가져 대칭적이지 않지만, 여기서는 대칭적이다. equality를 나타낸다.
• 다만 이것이 수학적 평등과 완전히 동일한 것은 아니다.
  
  
• 예: 7 = 3 + 4
  • 수학적으로는 참이지만, 논리 프로그램에서는 7과 3+4 모두 기저항이며 구문적으로 다르다.
  • 따라서 7 = 3+4는 해결 불가능(unsolvable)하다.
  
  
• f(X) = g(Y)는 해가 없다(서로 다른 함수 기호 f와 g).
• f(X) = f(g(X))? - 해 없음.
  • {X/g(X)}를 시도하면 X가 또 다시 g(X)를 포함하게 되어 끝없이 확장된다. f(g(g(X)))
  • f(X) = f(g(Y))? - 해 가능.

Unifier

• f(X) = f(g(Y))를 생각해보자. 이는 해결 가능하다.
• 가능한 해 중 하나: 𝒟 = { X/g(Y) }
• 𝒟를 적용하면 f(X) = f(g(Y))는 f(X)𝒟 = f(g(Y)) = f(g(Y))𝒟가 되어 참이다.
• 이때 𝒟를 equation의 두 term을 합일(unify)한다고 하며, 𝒟는 X와 g(Y)의 unifier라고 한다.

Most General Unifier, MGU

• f(X) = f(g(Y)) 문제에서 𝒟 = {X/g(Y)} 이외에도 다른 해가 있을 수 있다.
  • 예: { X/g(a), Y/a }, { X/g(f(W)), Y/f(W) } 등
• 그러나 이 solution들은 𝒟보다는 덜 일반적이다.
• 모든 solution은 𝒟와 다른 것들의 composition이다.
  • 따라서 𝒟를 X와 g(Y)의 가장 일반적인 합일자(Most General Unifier, MGU)라고 한다.
  
  
• 식 집합 E = { s1 = t1, ..., sn = tn }에 대해 si, ti가 term이라고 할 때,
• 치환 𝒟를 적용하여 (s1, ..., sn)𝒟와 (t1, ..., tn)𝒟가 구문적으로 동일해진다면 𝒟는 E의 합일자(unifier)이다.
• E의 모든 합일자 중 가장 일반적인 것이 MGU이다.

Unification Algorithm

=> 어떻게 MGU를 얻을 것인가?

• 모든 equation 집합에 대해 Unification Algorithm은 집합이 unifiable하면 MGU를 찾아내고, 아니면 실패를 반환한다.
• 원래는 로빈슨(Robinson)이 1965년에 개발했다.
  • 이후 더 개선된 다양한 Unification algorithm들이 제안되었다.
• 여기서는 1982년 Martelli와 Montanari의 unification algorithm을 다룬다.
  
• E = { s1 = t1, ..., sn = tn }이 주어졌을 때,
• 알고리즘은 실패나, 혹은 𝒮 = { X1 = r1, ..., Xm = rm } 형태의 equation set을 산출한다.
  • 여기서 Xi는 서로 다른 변수이고 r_i는 항이며 Xi는 r_i 안에 등장하지 않는다.
• 𝒮를 solvent form이라 하고, 여기서 MGU는 { X1/r1, ..., Xm/rm } 형태로 얻어진다.
  
• 알고리즘은 비결정적(non-deterministic)이다. 즉, 여러 선택지가 있을 때 임의로 하나를 선택할 수 있다.
  1. E에서 식 하나를 비결정적으로 선택한다.
  2. 선택한 식의 형태에 따라 특정 연산을 수행(또는 실패 종료)한다.
  3. 가능한 연산이 없으면 성공으로 종료하거나, 아니면 실패 종료 이외의 연산이 실행 된 경우 다시 1로 돌아간다.
  
  
• 연산 유형 및 동작:
  a) f(l1, ..., lk) = f(m1, ..., mk): 이 식을 E에서 제거하고, l1 = m1, ..., lk = mk를 E에 추가한다.
  b) f(l1, ..., lk) = g(m1, ..., mk): f ≠ g이면 실패 종료한다.
  c) X = X: 이 식을 E에서 제거한다.
  d) X = t:
  1. X가 t에 나타나지 않고(X ≠ t), X가 E의 다른 식에 등장하면 {X/t}를 E의 다른 식에 모두 적용한다.
  2. t 안에 X가 있다면 실패 종료.
  e) t = X: t가 변수가 아닐 경우 식을 E에서 제거하고 X = t를 E에 추가한다. (t와 X를 서로 바꿀 수 있다)

ex) f(t) = f(x)
a)에서 t = x를 얻고, 그 다음 X=t로 바꾼다.
d)로 가서 X = t, Y = f(X)에다가 f(t)로 해준다.

X = f(X)인 경우 terminate with failure

예제(Example)

• E = { f(X, b) = f(g(Y), W), h(X, Y) = h(Z, W) }. (a)
• f(X,b)=f(g(Y),W)에 (a)규칙 적용: E1 = { X = g(Y), b = W, h(X, Y) = h(Z, W) }
• t = X 형태에 (e)규칙 적용: E2 = { X = g(Y), b = W, h(g(Y), Y) = h(Z, W) }
• W = b 형태에 (d)규칙 적용: E3 = { X = g(Y), W = b, h(g(Y), Y) = h(Z, W) }

• h(g(Y), Y) = h(Z, W)에 (a)규칙 적용: E4 = { X = g(Y), W = b, h(g(Y), Y) = h(Z, b) }
• h(g(Y), Y) = h(Z, b)에 (a)규칙 적용: E5 = { X = g(Y), W = b, g(Y) = Z, Y = b }
• Y = b에 (d)규칙 적용: E6 = { X = g(Y), W = b, Z = g(Y), Y = b }
  
• Y에 b를 대입하면: E7 = { X = g(b), W = b, Z = g(b), Y = b }
• 이제 해결형이 되었고, MGU는 { X/g(b), W/b, Z/g(b), Y/b }이다.

41. 요약(Summary)
    • 일차 논리(First-order Logic)
    • 용어(Terminology)
    • 호른 절(Horn Clause)
    • 치환(Substitution)과 합일(Unification)
    • 가장 일반적인 합일자(Most General Unifier, MGU)
    • 합일 알고리즘(Unification Algorithm)