Written by JS970
on April 13, 2023

프로그래밍언어론 2023-04-13 수업정리

Flow

Axiomatic System(공리계)
- 공리의 유한 집합, 사실(fact)과 추론 규칙(rules)로 구성된다.
  - 사실(predicate) : 아래와 같이 표현 가능하다. 항상 참이다.$$\frac{true}{fact}$$
  - 추론 규칙(rules) : 가정(hypothetics) 술어들을 바탕으로 결론 술어를 도출해 내는 규칙이다. 아래와 같이 표현 가능하다.$$\frac{predicate^{\ *}}{predicate}$$$$predicate^{\ *} \models predicate$$
Hoare Logic$${P}\ S\ {Q}$$
- P, S, Q를 묶어서 Hoare Triple이라고 한다.
- P : 사전조건(input spec)
- Q : 사후조건(output spec)
- output spec으로부터 input spec이 derive된다면 올바른 program이다. 이때 input spec P의 최약 사전 조건(weakest Precondition)을 Axiomatic System을 통해 찾을 수 있다.
- output spec으로부터 input spec을 derive 할 수 있음을 증명하기 위해 몇 가지 Axiom을 배웠다.
  - Assignment Axiom
  - The rule of consequence
  - The rule of compostion
  - The rule of selection
  - The rule of iteration
- 특히 rule of iteration에서는 Invarient Variable I를 찾는 과정이 중요했다. I가 숨겨져 있으므로 직관적으로 판단하기가 힘들었다.

Procedural Language(순차적 프로그래밍 언어) : BASIC, FORTRAN, C++, Pascal, Java ...
- computational step을 하나하나 명시해야 한다.
- 이때 computational step이란 instruction, statement, procedure을 통한 계산 과정이다.
- 어떻게(how) 문제를 풀어야 하는지 기술한다.
Declarative Language(선언적 프로그래밍 언어) : LISP, Prolog, ML ...
- computational rules를 명시한다.
- fact는 computational rules의 special cases이다.
- 무엇(what)을 풀어야 하는지 기술한다.
Procedural Language, Declarative Language가 how와 what의 차이를 보이기는 하지만, 현실에서는 이 둘이 항상 확실히 구별되지는 않는다.
- 순차적 언어에도 what에 대한 특징이 있다.(타입 선언)
- 선언적 언어에도 how에 대한 특징이 있다.(Prolog의 cut)

1차 술어 계산(1st-order predicate calculus)을 기반으로 한다.
Rules(규칙) : Horn clause(Horn 절)을 이용하여 표시한다.
- Horn절은 Conjunctive Normal Form으로 생각하면 이해하기 쉽다.

interesting(L) :- lectureByWoo(L), language(L).

fact.

-? goal.

lectureByWoo(prolog).
lectureByWoo(scheme).
language(prolog).
language(scheme).

interesting(L) :- lectureByWoo(L), language(L).

?- interesting(prolog).
true.

?- interesting(scheme).
true.

?- interesting(cpp).
false.

?- edit(file('filename.pl')).

?- consult(filename).

?- [filename].

질의(목적의 명시)
- 당연하지만 parent rule이 명시되어 있어야 아래와 같은 질의가 가능하다.
- 답변에 만족했다면 질의 이후 "Enter" 입력
- 답변에 만족하지 않았다면 ";" 를 입력하여 계속 질의

?- parent(X, jim).

?- halt.

Top