2. 콕으로 프로그래밍하기


콕 시스템에서 프로그램은 보통 함수로 표현한다. 프로그램이 간단하면 이 시스템 자체에서 실행할 수 있고, 더 복잡하다면 일반적인 프로그래밍언어로된 프로그램으로 변환하여 시스템 밖에서 실행할 수도 있다.


2.1 상수 정의


키워드 Definition으로 상수를 새로 정의할 수 있다. 예를 보자.


Definition example := fun x : nat => x*x + 2*x + 1.


동일하지만 이렇게도 정의할 수 있다.


Definition example1 ( x : nat) := x*x + 2*x + 1.


이 명령어들을 실행한다음 다른 명령어로 이 함수를 다뤄볼수 있다.


Check example1.

example1 : nat -> nat


Eval compute in example1 1.

= 4 : nat


어떤 경우에는 이전에 만들었던 정의를 없애고 싶을수가 있다. Reset 명령어로 정의한 이름을 주면 가능하다. 정의한 내용을 보고싶으면 Print 명령어를 사용한다. Coqide나 Proof-General 같은 특별한 환경을 사용하고 있다면 작업창 상단의 화살표로 문서의 이곳 저곳으로 실행 포인트를 이동할수 있다.


2.2 부울 조건식

콕에 미리 정의되어있는 타입으로 부울값의 타입이 있다. true와 false 두가지 값을 갖는다. 부울식을 제대로 사용하려면 Bool 라이브러리를 불러야한다. 부울 곱, 합, 부정 등의 정의를 사용할수 있다.


Require Import Bool.


부울값은 if...then...else... 구문으로 검사할수 잇다.


Eval compute in if true then 3 else 5.

= 3 : nat


이 타입과 연관되어 사용할 수 있는 함수로 무엇이 있는지 알고 싶다면 Search나 SearchAbout 명령어를 사용할수 잇다. Search 명령어를 사용한 예를 보자.


Search bool.

false: bool

true: bool

xorb: bool -> bool -> bool

orb: bool -> bool -> bool

negb: bool -> bool

implb: bool -> bool -> bool

ifb: bool -> bool -> bool -> bool

eqb: bool -> bool -> bool

andb: bool -> bool -> bool



2.3 자연수로 계산하기

자연수의 타입도 콕에 준비되어있다. 이 타입을 제대로 사용하려면 역시 Arith 라이브러리를 불러야한다.


Require Import Arith.


자연수는 0부터 무한대까지의 숫자들이다. 자연수 나름의 조건식을 구성하는 방법이 있다. 모든 자연수를 0 또는 어떤 자연수 p의 그 다음 S p로 표현하는 아이디어를 이용한다. 즉, 1은 S 0, 2는 S (S 0)가 된다.


이런 방식에서는 모든 자연수가 0이거나 다른 수의 다음으로 두가지 경우로 나눌수 있다. 이런 구분 방식으로 함수로 작성하면 다음과 같다. 이 함수는 인자가 오직 0인 경우에만 true를 반환한다.


Definition is_zero (n : nat) := 

   match n with

     0 => true

   | S p => false

   end.


match ... with ... end 식을 패턴매칭 구문이라고 부른다. 이 식을 계산한 결과는 n의 패턴에 달려있다. 0의 패턴이면 true이고, S p 패턴에 맞으면 false가 된다. S p 패턴에서 기호 S는 무엇의 다음이라는 개념을 뜻하는데 만일 n이 S p 패턴과 일치하면 다음과 같이 직관적으로 해석할 수 있다. n은 어떤 수의 다음에 위치한 수다. 패턴에 나타난 p는 일종의 지역변수로 그 "어떤 수"를 받는다. 화살표 => 오른편의 식에 p를 자유롭게 사용할 수 있다.


패턴매칭은 자연수로 계산할때 자주 사용한다. 예를 들어, 콕 시스템에서 제공하는 pred 함수는 0보다 큰 자연수를 그 전에 위치하는 수로, 0은 0으로 매핑한다.


Print pred.

pred = fun n : nat =>

   match n with | 0 => n | S u => u end

        : nat -> nat


Argument scope is [nat_scope]


pred 함수는 패턴매칭 구문을 사용해서 S u 형태의 수는 u로, 0은 0으로 매핑하는 것을 표현한다.


자연수로 계산할때 재귀 형태가 흔히 나타난다. 패턴매칭을 사용하는 함수를 정의할때 이 함수에 인자의 이전 숫자를 주어 사용하는 것이 가능하다. 콕은 재귀 방식으로 정의된 것을 매우 조심스럽게 다루기 때문에 특별한 키워드를 함께 사용해야한다. Fixpoint 키워드이다. 두 자연수를 더하는 재귀함수의 예를 보자.


Fixpoint sum_n n :=

   match n with

       0 => 0

   | S p => p + sum_n p

   end.


재귀함수를 정의할때 구조적 재귀라는 제약을 고려해야한다. 재귀함수를 호출하려면 원래 인자의 부분식만을 인자로 취할수 있다. 더 정확히 말하자면, 재귀함수의 인자는 반드시 변수이고 패턴매칭을 통해서 원래 인자로부터 얻은 것이어야 한다. 이런 제약을 지키면 모든 계산이, 설사 재귀함수를 쓰더라도, 종료함을 보장할 수 있다. sum_n의 정의는 제대로된 형태를 갖추고 있다. 왜냐하면 원래 인자 n과 매치되는 S p 패턴의 변수 p만 사용하기 때문이다.


예를 들어, 구조적 재귀 제약을 지키지 않은 다음 정의는 사용할수 없다.


Fixpoint rec_bad n :=

   match n with 0 => 0 | S p => rec_bad (S p) end.

Error:

Recursive definition of rec_bad is ill-formed.

In environment

rec_bad : nat -> nat

n : nat

p : nat

Recursive call to rec_bad has principal argument equal to "S p" instead of

"p".

Recursive definition is:

"fun n : nat => match n with

                | 0 => 0

                | S p => rec_bad (S p)

                end".


여러개의 인자를 받는 재귀함수를 정의할수 있다. 이런 경우 이 인자들중 하나는 구조적 재귀 제약을 따라야 한다. 예를 들어 아래 함수는 합의 중간결과를 인자로 받아 첫번째 인자인 자연수를 누적해서 더한다. 첫번째 인자에 대해서 구조적 재귀 제약을 만족한다. 왜냐하면 재귀함수를 호출할 때 첫번째 인자 p는 원래 첫번째 인자 n을 패턴매칭해서 얻은 것이기 때문이다.


Fixpoint sum_n2 n s :=

   match n with

       0 => s

   | S p => sum_n2 p (p + s)

   end.


재귀함수를 정의할 때 부울 타입과 같이 다른 타입의 값을 반환하도록 정의할수도 있다. 자연수로 주어진 인자가 짝수인지 검사하는 함수가 그러한 예이다.


Fixpoint evenb n :=

   match n with

      0 => true

    | 1 => false

    | S (S p) => evenb p

   end.


이 예제에서 깊은 패턴매칭을 사용했고, 두가지 이상의 경우를 나열했다. 콕 시스템은 모든 경우를 커버하는지 검사하고 재귀함수호출에서 패턴매칭을 통해서 얻은 변수들을 인자를 사용하는지를 검사할 것이다.


2.4 리스트로 계산하기

같은 타입의 데이터를 리스트로 모아 다룰 수 있다. 물론 리스트를 사용하기 위해 필요한 라이브러리를 불러야한다.


Require Import List.


여러 원소를 모아 하나의 리스트를 만드려면 두개의 콜론 ::으로 구분해서 차례로 나열하고 맨끝에 ::nil을 둔다.


Check 1::2::3::nil.

1 :: 2 :: 3 :: nil

      : list nat


:: 표기법은 어떤 리스트 앞에 요소를 추가함을 뜻한다. nil은 원소가 없는 리스트이고, 3::nil은 원소가 오직 3을 가지고 있고, 2::3::nil은 3만 포함하는 리스트 앞에 2를 붙인 리스트다.


nil은 콕 시스템에서 특별하게 사용된다. 왜냐하면 사용되는 문맥에 따라 다르게 사용될 수 있기 때문이다. 요소를 포함하는 리스트에서는 이 원소와 동일한 타입에 대한 비어있는 리스트를 표현한다. 하지만 nil을 그 자체로만 쓰면 콕 시스템은 문맥을 판단하지 못해 적절히 해석하는데 어려움에 처하게 된다(콕 시스템의 버전에 따라 다름).


Check nil.

Error: Cannot infer the implicit parameter A of nil.


또는

nil

      : list ?1


이런 문제가 발생하면 nil을 사용할때 의도하는 문맥을 타입으로 콕 시스템에게 알려주어 해결할 수 있다.


Check (nil : list nat).

nil:list nat

    : list nat


리스트를 다루는 몇가지 함수들을 콕 시스템에서 제공한다. 리스트 붙이기 함수 app (보통 ++로 사용), 함수를 받아 리스트의 각각의 원소에 적용하는 함수 map 등이 있다.


Eval compute in map (fun x => x + 3) (1::3::2::nil).

= 4 :: 6 :: 5 :: nil : list nat


Eval compute in map S (1::22::3::nil).

= 2 :: 23 :: 4 :: nil : list nat


Eval compute in

   let l := (1::2::3::nil) in l ++ map (fun x => x + 3) l.

= 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: nil : list nat


리스트, map, app에 대한 연습문제

숫자 n을 입력받아 0부터 n-1까지 n개의 원소로 된 리스트를 반환하는 함수를 정의하시오.


리스트의 원소를 다룰때 패턴매칭 식을 사용한다. 자연수에 대한 패턴매칭과 유사하다. 리스트는 비어있거나 다른 리스트 앞에 원소를 갖는 두가지 경우로 분류할 수 있다. 두번째의 경우에 패턴매칭 식으로 리스트의 첫번째 원소와 나머지 리스트에 이름을 붙일 수 있다. 다음 예를 살펴보자. 인자로 주어진 리스트가 적어도 원소를 하나 포함하고 있고 첫번째 원소가 짝수이면 true를 반환하는 함수이다.


Definition head_evb l :=

   match l with nil => false | a::tl => evenb a end.


리스트에 대한 재귀함수를 정의할 수도 있다. 자연수를 다룰때와 동일하게 구조적 재귀 제약을 따라야 한다. 재귀함수 호출은 인자 리스트에서 직접적으로 얻은 부분리스트만 인자로 취할 수 있다. 리스트의 원소를 모두 더하는 예를 보자.


Fixpoint sum_list l :=

   match l with nil => 0 | n::tl => n + sum_list tl end.


마지막 예로, 자연수 리스트를 정렬하는 함수를 작성해보자. 두 자연수를 비교해서 부울값을 반환하는 함수 leb를 사용한다. 콕 시스템에서 제공한다.


Fixpoint insert n l :=

   match l with

       nil => n :: nil

   | a::tl => if leb n a then n::l else a ::insert n tl

   end.


Fixpoint sort l :=

   match l with

       nil => nil

   | a::tl => insert a (sort tl)

   end.


간단하게 테스트해보자.


Eval compute in sort (1::4::3::22::5::16::7::nil).

= 1 :: 3 :: 4 :: 5 :: 7 :: 16 :: 22 :: nil

     : list nat



정렬에 대한 연습문제

리스트를 인자로 받아 원소의 수가 2미만이거나 첫번째 원소가 두번째 원소보다 작을 때 true를 반환하는 함수를 작성하시오. 그 다음 역시 리스트를 인자로 받아 정렬되었는지 검사해서 true를 반환하는 함수를 작성하시오.


카운팅에 대한 연습문제

콕 시스템에서 제공하는 함수 beq_nat으로 두 자연수를 비교할수 있다. 이 함수를 이용하여 count_list를 작성하시오. 인자로 자연수와 리스트를 받아 이 자연수가 리스트 원소로 몇번 나타나는지 세어 그 횟수를 반환한다.


===

번역


(1장)

Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태


(2장)

Keyword : 키워드

Boolean : 부울

Conjunction : 곱

Disjunction : 합

Negation : 부정

Construct : 구문

Pattern-matching : 패턴 매칭

Recursivity : 재귀 형태

Structural Recursion : 구조적 재귀

Subterm : 부분식

Sublist : 부분리스트

Posted by lazyswamp :

Coq 증명기(http://coq.inria.fr/)는 수학과 알고리즘을 형식화해서 표현하고 여러 성질을 증명하는 도구입니다. 


Coq 증명기가 무엇인지 궁금하거나 배워보고 싶은 분들이 참고 할 수 있는 Yves Bertot의 "Coq in a Hurry"를 번역했습니다. 1장~8장까지 별도의 글로 나누어 올려놓았고, 9장과 10장은 연습문제와 해답으로 번역에서 제외했습니다.


특히, 프로그래밍언어, 정형기법, 논리, 컴파일러를 전공하거나 관심을 두신 분들이 이 글의 독자가 될 수 있을 것으로 생각합니다.


새로운 프로그래밍언어를 배울때 가장 좋은 방법은 자신만의 문제를 하나 선택해서 스스로 풀어보는 것이지요. 저도 이 글을 읽고 번역한 다음, 텍스트 패턴 매칭에 대한 어떤 성질을 증명해보고 있습니다. 좌충우돌... 그럼에도 불구하고 Coq에 조금씩 적응하고 있구나 하는 생각이 듭니다. Coq을 처음 배운다면 구문이 생각나지 않을 수 있고, 증명하는데 적절한 전술이 무었일까 답답할 수도 있습니다. 이런 경우 1장~8장을 뒤적이면 유용한 답을 찾을 수 있을 것입니다. 특히 초보자에게 가장 도움이 되는 부분은 3장이 아닐까 생각합니다.


마지막으로, 글쓰기도 어렵지만 번역은 더 어렵네요. 글을 읽으시다 잘 이해가 가지 않는 문장이 있으면 틀림없이 번역에 문제가 있을 것으로 추측됩니다. 잘못된 번역, 더 매끄러운 번역이 생각나시면 언제든지 댓글을 달아주세요. 


2014년 7월, 최광훈.



[원문]

Coq in a Hurry (Yves Bertot, April 2010)

 - http://cel.archives-ouvertes.fr/docs/00/47/58/07/PDF/coq-hurry.pdf




콕, 빨리 빨리 - 이브 베르토


이 글에서 콕 시스템을 간단히 소개하고 논리적 개념과 함수를 정의하고 추론하는 법을 일러준다. 일종의 튜토리얼이고, 독자들은 이 시스템의 몇가지만을 배워 하고싶은 것을 빨리 실험해볼 수 있다. 더욱 자세히 배우고 싶다면 참고문헌 [1]을 보면 된다. 특히 방대한 연습문제가 있어 훈련하기에 좋다.



 참고 문헌



[1] Yves Bertot and Pierre Cast ́eran. Interactive Theorem Proving and Program Devel- opment, Coq’Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.


[2] The Coq development team. The Coq proof Assistant Reference Manual, Ecole Polytechnique, INRIA, Universit de Paris-Sud, 2004. http://coq.inria.fr/doc/ main.html 


목차

 1. 식과 논리식

 2. 콕으로 프로그래밍하기

 3. 명제와 증명

 4. 숫자 프로그램의 성질을 증명하기

 5. 리스트 프로그램의 성질을 증명하기

 6. 새로운 데이터 타입 정의하기

 7. 콕 시스템의 숫자

 8. 귀납적 성질

 9. 연습문제 (원문 참고)

 10. 해답 (원문 참고)



1. (계산?)식과 논리식


콕 시스템은 일종의 언어를 제공한다. 이 언어로 논리식을 다루고, 구문 형태를 살피고, 증명하기도 한다. 논리식은 함수를 사용하여 구성하기도 하고, 제한된 형태지만 이 함수들을 가지고 계산도 한다.


1.1 바른 식 쓰기


먼저 식이 제대로 된 형태인지 검사하는 법을 배울 필요가 있다. 이 명령어는 Check이다. 몇가지 예를 들어보자. 이 시스템의 기초적인 객체와 타입을 두세가지 사용한다. 명령어는 항상 점으로 끝난다. 이제부터 사용자가 콕 시스템에 보내는 글은 이런 스타일이고, 이 시스템에서 응답하는 내용은 이런 스타일이다. 


Check True.

True : Prop


Check False.

False : Prop


Check 3.

3 : nat


Check (3+4).

3 + 4 : nat


Check (3=5).

3=5 : Prop


Check (3,4).

(3,4) : nat * nat


Check ((3=5)/\True).

3 = 5 /\ True : Prop


Check nat -> Prop

nat -> Prop : Type


Check (3 <= 6).

3 <= 6 : Prop


두가지 목적으로 A : B 표기법을 사용한다. 식 A의 타입이 식 B이다거나 A는 B의 증명임을 나타낸다. 우리가 입력하는 식에서도 이 표기법을 사용할 수 있다. 보통 어떤 식의 타입을 분명히 드러내고자할때 그렇다. 


Check (3,3=5):nat*Prop

(3,3=5):nat * Prop

       : nat * Prop


이 식들 중 어떤 것은 논리 명제로 읽고 (즉  Prop 타입을 가지고) 또 어떤 것은 숫자로 읽고(nat 타입을 갖고), 다른 것은 더 복잡한 자료구조의 원소로 읽기도 한다. 물론 제대로 형태를 갖추지 못한 식도도 검사해볼수 있다. 이 경우 콕 시스템은 에러문을 출력해 문제점을 설명해줄것이다.


복잡한 식을 구성하려면 명제들을 논리 연결자들로 조합하거나 덧셈, 곱셈, 쌍만들기 등으로 식들을 구성하면된다. 키워드 fun을 사용해서 새로운 함수도 만들수 있다. 람다계산법과 같은데에서 lambda 기호대신 쓴다. Check 명령어로 함수를 검사하면 nat 타입의 숫자 x를 입력으로 받아 x가 3과 같다는 명제를 리턴한다고 설명해준다. 그 다음 Check 명령어에서 검사하는 논리명제는 모든 자연수 x에 대해 x는 3보다 작거나 또는 자연수 y가 존재해서 x=y+3이다.


Check (fun x:nat => x=3).

fun x : nat => x = 3 : nat -> Prop


Check (forall x:nat, x<3 \/ (exists y:nat, x=y+3)).

forall x:nat, x<3 \/ (exists y:nat, x=y+3) : Prop


이번에는 let을 사용하는 식을 살펴보자. 식에 임시 이름을 부여할 때 유용하다. 예제에서 let으로 이름을 붙인 식은 숫자를 입력받아 숫자의 쌍을 반환하는 함수다. 함수 f를 어떤 값, 예를 들어 3에 적용하는 표기 방법도 보여준다. 단순히 함수 이름 f와 인자 3을 나란히 쓰면된다. 보통 수학에서 하던것과 달리 인자를 감싸는 괄호를 항상 쓰지 않아도 된다. 


Check (let f := fun x => (x * 3, x) in f 3).

let f := fun x : nat => (x * 3, x) in f 3 : nat * nat 


어떤 표기법은 다용도로 사용된다. 예를 들어, * 기호는 곱셈을 표시하기도 하고 타입에서 곱을 표시하기도 한다. Locate 명령어로 표기법이 의미하는 함수를 찾을 수 있다.


Locate "_ <= _".

Notation Scope

"x <= y" := le x y : nat_scope

                    (default interpretation)


텀의 형태가 제대로 되려면 두가지 조건을 갖춰야한다. 정해진 구문을 따라야한다. 예를 들어, 열린괄호와 닫힌괄호의 쌍이 맞아야 하고 두개의 피연산자를 요구하는 연산자에게는 그렇게 인자가 주어져야한다. 두번째 조건은 타입에 맞게 식을 구성해야한다. Check 명령어는 식이 제대로 구성되었는지 검사도 하고 식의 타입을 알려주기도한다. 예를 들어 어떤 식이 제대로 되었는지 차근차근 단계별로 확인할 수 있다.


Check True.

True : Prop


Check False.

False : Prop


Check and.

and : Prop -> Prop -> Prop


Check (and True False).

True /\ False : Prop


마지막 예에서 and는 Prop 타입의 인자를 받아 Prop -> Prop 타입의 함수를 반환하는 함수다. 따라서 Prop 타입의 True에 적용할 수 있다. 그 결과 반환되는 함수는 또다른 Prop 타입의 인자를 기대하고 False에 적용할 수 있다. 표기법 a -> b -> c는 사실

a -> (b -> c)이다. 표기법 f a b는 사실 (f a) b 이다.


그리고 /\는 피연산자들 가운데에 연산자를 배치하는 인픽스 표기법을 따른다. Locate 명령어로 확인할 수 있다.



2. 식을 계산하기


콕 시스템으로 식을 계산할 수도 있다. 기호 계산 방식을 사용하는데, 여러가지 전략이 있다. compute라고 부르는 전략은 다음과 같이 사용한다.


Eval compute in 

   let f := fun x => (x * 3, x) in f 3.

= (9, 3) : nat * nat


이 명령어를 실행한 뒤에는 함수 f가 사라진다. 이 식을 계산할 때 임시로 정의되고 f 3을 계산할 때 사용될 뿐이다.


함수에 관한 연습문제 (참고문헌 [1]의 연습문제 2.5) 다섯개의 인자를 받아 그 합을 반환하는 함수를 작성하고, Check 명령어로 제대로된 형태로 작성했는지 확인한 다음, Eval 명령어로 샘플 값들을 주어 계산해보시오.  연습문제에 대한 답은 모두 이 글의 마지막에 제공한다.




===

번역


Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태



Posted by lazyswamp :