[이산수학] 오퍼레이션 (암시적 정의/명시적 정의)

<< 이산수학 2주차 >>

Operation
값을 받아서(argument), 처리하여, 결과(result)를 출력한다.

type vs 변수
- 변수의 타입은 변수가 가질 수 있는 값의 집합
- 변수는 해당 타입에서 하나의 값을 가진다.
- 변수에 비해서 타입이 반드시 한 차원 높다.  // x(변수) : int(타입)

오퍼레이션 형식
ex) 정수 오퍼레이션 Z, 이진 집합 B
+ : Z x Z -> Z
- :  Z x Z -> Z
* : Z x Z -> Z
= : Z x Z -> B

변수는 type에 속할 수 있다? O, 가능하다.

※ 자주 사용되는 집합들 (자연수/정수/실수 집합 등)

자주 사용되는 집합 모음

----------------------------------------------------------------------------------------------------------

문자열 Operation
A가 문자 집합이면, A*는 모든 문자열 집합이다.

표현) <t,e,n,n,i,s> = "tennis" 등과 같이 표현

★문자와 문자열을 구분해야한다.★
 - "t" ∈ A  // t 문자열은 문자에 속하나? X
 -  t ∈ A* // t 문자는 문자열에 속하나? X
 - "tennis" ∈ A* // tennis 문자열은 문자열에 하나? O
 - < > ∈ A // 꺽쇄(공백 문자열) 문자에 속하나? X
 - < > ∈ A* // 꺽쇄(공백 문자열) 문자에 속하나? O

ex) 문자열 결합 오퍼레이션 : strcat : A* x A* -> A*
     문자열 길이 오퍼레이션 :    len : A* -> N0
          // 길이는 0 이상을 포함하기 때문에 0을 포함하는 자연수에 속함.

정의 
- 명시적 정의 : 이미 정의된 것을 이용하여 결과를 구하는 과정을 정의 //그레이-박스 관점
- 암시적 정의 : 과정보다는 입력과 출력의 과정을 이용함 // 블랙-박스 관점
- 알고리즘적 정의 : 결과를 구하는 과정이 상세함 // 화이트-박스 관점

1. 명시적 정의 
(제곱함수)
square : R -> R
square(x) = x*x

(팩토리얼 함수)
fact : N0 -> N
fact(n) = if(n=0) then 1 else fact(n-1)*n
- fact(0) = 1 // 종료 조건
- fact(n) = fact(n-1)*n // 재귀 조건, 0을 만나면 stop 한다


(head, 첫번째 문자 구하기)
- 함수 선언 : head : A* -> A
- 함수 정의 : head(<a1, a2, ... an>) = a1
- 보조 설명 : head(<>) undefined
                 head(<a1, a2, ... , an>) = a1 ≠ <a1> // 중요한 부분은 '문자'가 리턴되는 것임

(tail, 첫번째를 제외한 나머지 문자열 구하기)
- 함수 선언 : tail : A* -> A*
- 함수 정의 : head(<a1,a2, ... , an>) = <a2, ... , an>
- 보조 설명 : head(<>) undefined

(strcat, 문자열 결합)
함수 선언 : strcat A* x A* -> A*
함수 정의 : strcat(< ... >, < ... >) = < .... >
보조 설명 : strcat 대신 || 기호 사용
  결합 법칙 만족 S1 || S2 || S3 = (s1|| s2) || s3 = s1 || (s2 || s3)

**정리 If S ∈ A* and S≠< > then S <head(S)> || tail(S)
"tennis"
= <head("tennis")> || tail("tennis") // t에 <>를 사용하여 문자를 문자열로 변환한 후, 결합
= "t" || "ennis"
= "tennis


(len, 문자열 길이 리턴)
함수 선언 : len : A* -> A0
함수 정의 : len(<>) = 0
  len(S) = len(tail(S))+1 // tennis에서 t를 제외한 길이 = 5+1 = 6
    // 마지막 len("s") 일때, s를 제외한 tail부분이므로 len(<>)=0 이 된다.

(index, 해당 위치의 문자)
함수 선언 : index : A* x N -> A  // 문자열에서 N(index)를 넣으면 A(문자)가 리턴
함수 정의 : index(S,1) = head(S)
  index(S,n) = index(tail(S), n-1)
주의 : S(n)으로도 표기 가능, n의 범위는 0＜n≤len(S)
예시 : index("tennis", 3)
         = index("ennis", 2)
         = index("nnis", 1)
         = n

(그 외 문자열 조작 함수)
dels : A* x N -> A*               // 문자열(A*)에서 N번째를 삭제하여 문자열을 리턴
mods : A* x N x A -> A*        // 문자열(A*)에서 N번째를 문자(A)로 대체하여 문자열을 리턴
subs : A* x N x N0 -> A*       // 문자열(A*)에서 N번째(from)부터 N개(to) 문자열을 리턴
front : A* x N0 -> A*            // 문자열(A*)에서 N0개의 문자열을 리턴
last : A* -> A                      // head와 반대 맨마지막에 잇는 문자를 리턴
rev : A* x N0 -> A*              // N0개까지의 Reverse된 문자열을 리턴


(dels, 특정위치의 문자 삭제)
함수 선언 : dels : A* x N -> A*
함수 정의 : dels(S,n) = if n>len(S) then S           //n이 길이보다 크다면 그냥 원래 문자열 리턴
  else if n=1 then tail(S) //n=1이면 S 삭제
  else <head(S)> || dels(tail(S), n-1) //(헤드 보관) || (S에서 n-1번째 삭제) 결합

**예외처리를 할 때, N은 0을 포함하는 자연수 이므로 n<0는 고려하지 않는다.

(mods, 특정 위치의 문자 수정)
함수 선언 : mods : A* x N x A -> A*
함수 정의 : mods(S,n,a) = if   n＞len(S)   then   S
       else   if n=1   then || tail(S) 
       else   n≤len(S)   then   <head(S)>   || mods(tail(S), n-1, a)

(front, 앞쪽 문자열 구하기)
함수 선언 : front : A* x N0 -> A*
함수 정의 : front(S,n) = if   n> len(S)   then   S
     else if   n=0   then   <>
     else   <head(S)> || front(tail(S,n-1))

(subs, 문자열에서 부분 문자열 리턴)
함수 선언 : subs : A* x N x N0-> A*
함수 정의 : subs(S,n,k) = if   s+k> len(S)   then   S
    else if   n=0   then   <>
    else   subs(tail(S)k, n-1, k)

(reverse, 반대로 된 문자열 리턴)
함수 선언 : rev : A* -> A*
함수 정의 : rev(S) = if   len(S)=0   then   <>
             else if   len(S)>0    then    reverse(tail(S)) || <head(S)>

  rev(S) = if   len(S)=0   then  <>
             else if   <last(S)> || rev(front(tail(S), len(S)-1))
 


■함수의 선행 조건■
잘못된 입력 값에 대비하기 위해 default value를 제공한다.
(if - 예외처리) // 그전까지의 함수 선언은 N을 사용하여 0의 경우를 제외함

Pre-condition
선행조건
- 입력되는 정의역을 제한하는 함수
- 선행 조건에 위배되면 값이 미정의
- 예외 처리를 고려하지 않아서 편리하다.

예시) dels : A* x N -> A*
       pre-dels : A* x N -> B //선행조건 (술어)
       pre-dels(S,n) = n≤len(S)

선행조건만 만족하는 범위 내에서만 정의하겠다.

선행조건을 이용하여 함수 재정의
입력되는 문자가 문자열의 길이를 초과하는 경우에는 문자열을 건드리지 않고 그대로 출력하는 대신에, 선행 조건을 이용해서 정의역을 제한해보자.

1. mods : A* x N x A -> A*
pre-mods(S, n, a) = n≤len(S) //n이 S의 길이보다 작아야 함.

2. front : A* x N0 -> A*
pre-front(S,n) = n≤len(S)
front(S,n) =   if   n=0   then   <>
                 else   || front(tail(S), n-1)​

3. subs : A* x N x N0 -> A*
pre-subs(S,n,k) = n+k ≤ len(S)
subs(S,n,k) = if   n=1   then   front(S,k)
                 else   || subs(tail(S), n-1, k)​

 

2. 암시적 정의 
 : 입력과 출력의 관계로 함수를 정의한다.
- 후행조건(post-condition) : 출력되는 치역을 제한하는 함수
- 선행 조건과 후행 조건으로 함수를 암시적으로 정의할 수 있다.

예제) 평균 함수
avg : N0 x N0 x N0 -> R
pre-avg : N0 x N0 x N0 ->B
pre-avg(x,y,z) : x, y, z ≥ 0
post-avg : N0 x N0 x N0(입력 세개) x R(출력) -> B   // 입력과 출력을 확인하여 boolean으로 리턴해줌
post-avg(x,y,z,result) ={ result = (x+y+z)/3 }


명시적 정의는 모두 암시적 정의로 변환할 수 있다.
- f(x1, ... , xn) = E // 명시적 정의
- post-f(x1, ... , xn, result) = { reulst = E }

암시적 정의는 프로그램 명세에 유용하게 쓰임
마치 블랙박스라고 설명을 했는데, "선행조건 -> (블박/암시적 정의) -> 후행조건"의 과정을 따름. 

(연습)
1. mods
mods : A* x N x A -> A*
pre-mods(S,n,a) = n≤len(S)
post-mods(S,n,a,result) =  ( result(n) = a ∧
∀i∈N, 모든 위치(i=n인 i≤len(S))의 문자열은 result(i) = S(i)
len(result) = len(S) )

2. sub
subs : A* x N x N0 -> A*
pre-subs(S,n,k) = n+k≤len(S)
post-subs(S,n,k,result) =  ( len(result) = k+1 ∧
∀i∈N (i≤len(result)-1) -> result(i+1) = S(n+1) )

3. front
front : A* x N -> A*
pre-front(S,n) = n≤len(S)
post-front(S,n,result) =  ( len(result) = n
∀i∈N (i≤len(result)) -> result(i) = S(n) )
 
------------------------------------------------------------------------------------

프로그램 명세 : what to do를 기술
프로그램 코드 : how to do를 기술

명세 = 타입 + 오퍼레이션
(코드 = 데이터 + 프로시져)

(예제) 사원 DB
- 타입
{ Employees, Id, Name, Age, Grade, Salary }
Employees = Id -> (Name x Age x Grade x Salary) // 함수 형식(테이블)

- 오퍼레이션
delete : Emplyees x Id -> Emplyees
add : ...
get : ...

- 암시적 정의
delete : Employees x Id -> Employees
pre-delete(E, eid) = eid ∈ dom(E)
post-delete(E, eid, result) =  //result는 변경된 DB
 현재 DB에서 e가 존재하는지, 

add : Employees x Id x Name x Age x Grade x Salary -> Employees
pre-add(E,eid,n,a,g,s) =  // eid가 dom(E) 재직 중이면 안됨
post-add(E,eid,n,a,g,s,result)
 현재 DB에 e가 추가되었는지

get : Employees x Id -> Name x Age x Grade x Salary
pre-get(E,eid) // 재직 중
post-get :   // result 값은 

ch_name : Employees x Id x Name -> Employees
pre-ch_name(E,eid,name) //eid가 재직 중
post-ch_name //result는 기존에 있던 data는 유지 & 변경하려는 data는 name만 변경

ch_age

(예제) 자동차 재고 수량
- 타입 : {DB, Body, Color, Engine, N0, N} // 이때 DB는 함수
          DB  = (Body x Color x Engine) -> N0

- 오퍼레이션
{init, add, howmany, withdraw}
init : ->DB
add : DB x Body x