요약

1. SW공학 수업의 핵심 주장:

SW is not a function but a dynamic sytem(state transition machine)
dynamic system의 구성요소

a. 초기자원

b. 상태변환규칙들

c. 최종상태


변환방식

옛날 방식
specification -> 프로그램 -> 자바 코드

새로운 방식
specification -> 프로그램 -> 상태변환 기계 [C interpreter or Java or prolog...]


2. Why linear logic is important.
계발시간이 짧아진다.

ex) sum(n) = 1+2+3+ ... + n을 프로그램하시오.
상태변환기계..

초기자원 : <1,1>

변환규칙 : <N,Y> -> <N+1, Y+N+1>

linear logic programming:
sum(1,1).
!∀N ∀Y (sum(N,Y) -o sum(N+1, N+Y+1)).

ex2) gcd(n,m) = the greatest common divisor of n and m

gcd(n,m) = gcd(n+m, m) if n>m.

gcd(4,2) =2
gcd(10,6) = gcd(16,6)=gcd(22,6)

초기자원 : ∀N, <N,N,N>, <N,1,1>

상태변환규칙 : ∀M,N,K,
rule1. <M,N,K> -> <N+M,N,K> if M>= N | K<N
rule2. <M,N,K> -> <N,M,K> if M>=N.
rule3. <M,N,K> -> <M+N,N,k> if M < N


linear logic
ex) !coffee |- coffee x coffee
yes

!coffee |- coffee & coffee
yes

!coffee |- coffee & milk
no why? 커피자판기에서 우유를 얻을 수 있나????????????????????????

coffee x coffee |-  !coffee
no 커피 2잔인데 자판기를 얻을 수 있나??????????????????



ex) !coffee |- coffee x coffee의 증명

coffee|-coffee     coffee |- coffee
--------------!D ---------------- !D
!coffee|-coffee    !coffee|-coffee
------------------------- &R
!coffee |- coffee & coffee

BMW & Excel |- Excel + pony 증명
BMW & Excel |- pony
-----------------------------  => 길을 잘 못 골랐다.
BMW & Excel |- Excel + pony

Excel |- Excel
----------------------
BMW & Excel |- Excel
-----------------------------  => 증명된다.
BMW & Excel |- Excel + pony


⅋ 곱하기 OR
A⅋B 두 개중에 최소한 한개는 가진다.
AxB 둘 다 가지는것


A⊸B A가 있으면 B로 바꿀 수 있다.
A가 없으면 B를 가질 수 도 있고 못 가질 수 있다. 상관없다.

A'⅋B A가 없으면 B는 don't care 있으면 B가 있어야 함(여기서 ' 은 not)

따라서 A⊸B ≡ A'⅋B

claim : the above machine is correct in the sense that if gcd(N,M,K) is true,
then it can be readched from the initial resource via the transition ruels.