차례 SNU 4190.210 프로그래밍원리 (Principles of Programming) Part I Prof. Kwangkeun Yi 1 프로그래밍기본부품과조합 (elements & compound) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) School of Computer Science & Engineering 5 타입으로정리하기 (types & typeful programming) 6 맞는프로그램인지확인하기 (program correctness) 다음 프로그램구성에필요한요소 1 프로그래밍기본부품과조합 (elements & compound) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) 5 타입으로정리하기 (types & typeful programming) 기본부품 (primitives) 조합하는방법 (means of constructing compound) 프로그램실행과정의이해 (rule of evaluation) 타입으로정리하는방법 (types) 속내용을감추는방법 (means of abstraction) 6 맞는프로그램인지확인하기 (program correctness)
기본부품의반복된조합 기본부품 (primitives) (pictures from Google search) 컴퓨터프로그램이다른점 : 만든것이실행 ( 계산 ) 된다 기본적으로제공됨. 상수 (constant) 라고도불림. type elements operators N, R 0, -1, 1.2, -1.2e2 +, *, /, =, <=, B #t, #f and, or, not, String "snow", "12@it" substr, strconcat, Symbol snow, 12@it Unit () 기본타입들 : N, R, B, String, Symbol 실행 (evaluation, semantics): -1.2e2는 1.2 10 2, #t는참, + 는 +, snow는 snow 라는심볼, 등 식을조합하는방법 프로그램식의실행과정 P ::= E program E ::= c constant x name (if E E E) conditional (cons E E) pair (car E) selection (cdr E) selection (lambda (x ) E) function (E E ) application 재귀적 (inductive, recursive): 만들수있는식은무한히많음식안에임의의식들을맘껏조합할수있슴 조합식의실행 (semantics) 은어떻게될까? 그실행을 머릿속에그려야. 주어진프로그램식을읽고 (read) 그식을계산하고 (evaluate) 계산중에컴퓨터메모리와시간을소모계산중에입출력이있으면입출력을수행 최종계산결과가있으면화면에프린트한다 (print) 주의 : 식의실행규칙 (rule of evaluation, semantics): 명확히정의됨 프로그래머는이것을이해해야의도한프로그램을작성할수있슴 제대로실행될수없는 ( 오류있는 ) 멀쩡한식들이많음
식의실행규칙 (rule of evaluation, semantics) 실행규칙. 각식의종류에따라서 : c 일때 : x 일때 : (if E E E) 일때 : (cons E E) 일때 : (car E) 일때 : (cdr E) 일때 : (lambda (x ) E) 일때 : (E E ) 일때 : 주의 : 생긴게옳다고모두제대로실행되는게아님 부품식들의계산결과의타입이맞아야 이름의사용, 이름의유효범위 (scope) 프로그램식조합방식의원리 모든프로그래밍언어에는각타입마다그타입의값을만드는식과사용하는식을구성하는방법이제공된다. 이원리를확인해보면 다음 1 프로그래밍기본부품과조합 (elements & compound) 타입 τ 만드는식 사용하는식 기본타입 ι c +, *, =, and, substr, etc 곱타입 τ τ (cons E E) (car E), (cdr E) 함수타입 τ τ (lambda (x ) E) (E E ) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) 5 타입으로정리하기 (types & typeful programming) 6 맞는프로그램인지확인하기 (program correctness)
이름짓기 (binding, declaration, definition) 이름짓기는속내용감추기 (abstraction) 의첫스텝 : 이름을지으면지칭하는대상 ( 속내용 ) 대신에그이름을사용 이름의유효범위 (scope) 결정 프로그램텍스트에서쉽게결정됨 (lexical scoping) 이름지을수있는대상 : 프로그램에서다룰수있는모든값 이름의유효범위 (scope) 가한정됨. 따라서, 이름재사용가능 전체프로그램의모든이름을외울필요없슴 이름이필요한곳에만알려짐 이름의유효범위 (scope) 는쉽게결정됨 이런간단한유효범위는수리논술의 2000 년전통 : Theorem The intersection of all addition-closed sets is addition-closed. Proof Let S be the intersection set. of S. Because x and y are elements of... Let x and y be elements hence in S. 이름짓기 (binding, declaration, definition) 식에서이름짓기 E ::= 예전것들 (let ((x E) + ) E) x의정의 (letrec ((x E) + ) E) x의재귀정의 프로그램에서이름짓기 P ::= E 계산식 (define x E) E 이름정의후계산식 이름짓기의실행규칙 (rule of evaluation, semantics) (let ((x E E) (letrec ((x E E) (define x E) E 주의 : 생긴게옳다고모두제대로실행되는게아님 부품식들의계산결과의타입이맞아야 이름의유효범위 (scope) 환경 (environment): 이름과그대상 ( 값 ) 의목록표
이름의유효범위 (scope) 예 이름짓기 + 사용하기의실행과정 (semantics) 컴퓨터는프로그램식을실행할때 이름과그대상의목록표를관리 그러한목록표를환경 (environment) 이라고함 a 1 b 2 env (( a 1) ( b 2 f (lambda (x) (+ x 1 이름짓기 + 사용하기의실행과정 (semantics) 여러개한꺼번에이름짓기 : 실행의미 환경 (environment) 관리 환경만들기 : 이름이지어지면 환경참조하기 : 이름이나타나면 환경폐기하기 : 유효범위가끝나면 (let ((x 1 E 1 ) (x 2 E 2 E) (letrec ((x 1 E 1 ) (x 2 E 2 E) (define x 1 E 1 ) (define x 2 E 2 ) E
설탕구조 (syntactic sugar) 편리를위해서제공 ; 지금까지것들로구성가능 ; 반드시필 요는없다 : list, cond, let, define 은설탕 (list E ) = (cons ) (cond (E E ) (else E = (if ) (let ((x E E ) = ((lambda ) ) (let ((x 1 E 1 ) (x 2 E 2 E) = ((lambda ) ) (define x E) E = (letrec ) (define x E) (define y E ) E = (letrec ) (define (f x) E) = (define ) (begin E E ) = ((lambda ) ) 다음 1 프로그래밍기본부품과조합 (elements & compound) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) 5 타입으로정리하기 (types & typeful programming) 6 맞는프로그램인지확인하기 (program correctness) 재귀 (recursion): 되돌기, 같은일의반복 예 ) 재귀하고있는그림들 : 예 ) 재귀하고있는표기법 : E ::= c x (if E E E) (cons E E) 예 ) 재귀하고있는정의 : a 0 = 1, a n+1 = a n + 2 (n N) X = 1 X 재귀함수 (recursive function) 의정의 함수만재귀적으로정의가능 ( 대부분의언어 ) ( 왜?) (define fac (lambda (n) (if (= n 0) 1 (* n (fac (- n 1 임의의값을재귀적으로정의? 그값계산이무한할수있슴 (define x (+ 1 x (define K (cons 1 K (define Y (cons 1 (add1 Y)
재귀함수의실행과정 끝재귀 (tail recursion) 변환 (define (fac n) (if (= n 0) 1 (* n (fac (- n 1) (define (fac n) 누적됨 : 재귀호출을마치고계속해야할일들이 함수호출때호출마치고계속해야할일 (continuation) 을기억해야 현대기술은재귀호출때누적않되도록자동변환 (define (fac-aux m r) (if (= m 0) r (fac-aux (- m 1) (* m r (fac-aux n 1 끝재귀 (tail recursion) 변환 끝재귀함수 (tail-recursive ftn) 의실행과정 고차함수 (higher-order function) 함수가인자로 b 함수가결과로 n=a 현대프로그래밍에서 f(n) = f(a) + + f(b) d f(x + ɛ) f(x) f(x) = dx ɛ 할일을 ( 하고 ) 재귀호출변수로전달 재귀호출마치고할일이누적되지않음 모두지원되는 (Scala, Python, Lua, JavaScript, Clojure, Scheme, ML, C#, F# 등 ) 과거에는지원되지못했던
고차함수는일상에서흔하다 고차함수의쓸모 고수준으로일반화된함수를정의할수있다 함수가인자로 요리사 ( 함수 ) 는요리법 ( 함수 ) 과재료를받아서... 댄서 ( 함수 ) 는리듬있게움직이는법 ( 함수 ) 과음악을받아서... 컴퓨터 ( 함수 ) 는프로그램 ( 함수 ) 과입력을받아서... 함수가결과로 요리학교 ( 함수 ) 는요리사 ( 함수 ) 를만들어내고댄스동아리 ( 함수 ) 는댄서 ( 함수 ) 를만들어내고컴퓨터공장 ( 함수 ) 은컴퓨터를 ( 함수 ) 만들어내고 (define (sigma lower upper) (lambda (f) (define (loop n) (if (> n upper) 0 (+ (f n) (loop (+ n 1) (loop upper) (define one-to-million (sigma 1 1000000 (one-to-million (lambda (n) (* n n) (one-to-million (lambda (n) (+ n 2) 고차함수의쓸모 다음 고수준으로일반화된함수를정의할수있다 (define (sum lower upper f) (if (> lower upper) 0 (+ (f lower) (sum (+ lower 1) upper f (define (generic-sum lower upper f larger base op inc) (if (larger lower upper) base (op (f lower) (generic-sum (inc lower) upper f larger base op inc (sum 1 10 (lambda (n) n (sum 10 100 (lambda (n) (+ n 1) (generic-sum 1 10 (lambda (n) n) > -1 + (lambda (n) (+ 2 n) (generic-sum "a" "z" (lambda (n) n) order "" concat alpha-next) 1 프로그래밍기본부품과조합 (elements & compound) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) 5 타입으로정리하기 (types & typeful programming) 6 맞는프로그램인지확인하기 (program correctness)
계산복잡도 (complexity) 프로그램실행비용의증가정도 (order of growth) 계산비용 = 시간과메모리 증가정도 = 입력크기에대한함수로, 단 관심 : 입력이커지면결국어떻게될지 (asymptotic complexity) 계산복잡도 (complexity, order of growth) 가 Θ(f(n 이다 (n은입력의크기 ), 만일그복잡도가 f(n) 으로샌드위치될때 : 계산복잡도 (complexity) (pictures from Google search) k 1 f(n) k 2 f(n) (k 1, k 2 는 n 과무관한양의상수 ) n 2, 10000 n 2, 3 n 2 + 10000 n 은모두 Θ(n 2 ) 계산복잡도 (complexity) 다음 (fac n): 시간복잡도 Θ(n), 메모리복잡도 Θ(n). (exp b n): Θ(n) 로구현가능 Θ(log n) 로구현가능 (sat formula): Θ(2 n ) 로구현가능 Θ(poly(n 로구현가능? 누구도모름 (diophantine eqn): Θ(2 n ) 로구현가능? 누구도모름 Θ(n n ) 로구현가능? 누구도모름 1 프로그래밍기본부품과조합 (elements & compound) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) 5 타입으로정리하기 (types & typeful programming) 6 맞는프로그램인지확인하기 (program correctness)
타입 (type) 사용하는타입들 (types) 타입 (type) 은프로그램이계산하는값들의집합을분류해서요약하는데사용하는 언어 이다. 타입으로분류요약하는방식은대형프로그램을실수없이구성하는데효과적이다. 타입 (type) 은가이드다 프로그램의실행안전성을확인하는새로운종류의데이터값을구성하는 τ ::= ι primitive type τ τ pair(product) type τ + τ or(sum) type τ τ ftn type, single param τ τ τ ftn type, multi params any type t user-defined type s name τ t user-defined type s name, with param ι ::= int real bool string symbol unit 고차함수타입 타입을상상하며식을구성하기 고차함수타입예 : int int (int int) int (real real) (real real) int (int int) int int (int int) int int (int int) int (int int) int list int (int int) int list int money (year car list) c : ι x : τ (if E:B E :τ E :τ) : τ (lambda (x:τ) E:τ ) : τ τ x : τ 임을 E 를구성할때기억 (E:τ τ E :τ ) : τ (cons E:τ E :τ ) : τ τ (car E:τ τ ) : τ (cdr E:τ τ ) : τ
타입을상상하며식을구성하기 타입을상상하며식을구성하기 c : ι x : τ (if E:B E :τ E :τ) : τ (lambda (x:τ) E:τ ) : τ τ x : τ 임을 E 를구성할때기억 (E:τ τ E :τ ) : τ (let ((x 1 :τ 1 E 1 :τ 1 ) (x 2 :τ 2 E 2 :τ 2 E:τ) x1 : τ 1 이고 x 2 : τ 2 임을 E 를구성할때기억 (letrec ((x 1 :τ 1 E 1 :τ 1 ) (x 2 :τ 2 E 2 :τ 2 E:τ) x1 : τ 1 이고 x 2 : τ 2 임을 E 1, E 2, E 를구성할때기억 (define x 1 :τ 1 E 1 :τ 1 ) (define x 2 :τ 2 E 2 :τ 2 ) E:τ (cons E:τ E :τ ) : τ τ (car E:τ τ ) : τ (cdr E:τ τ ) : τ x1 : τ 1 이고 x 2 : τ 2 임을 E 1, E 2, E 를구성할때기억 타입으로프로그램을정리 / 검산하기 타입으로프로그램을정리 / 검산하기 (define (fac n) (if (= n 0) 1 (* n (fac (- n 1) (define (fibonacci n) (cond ((= n 0) 0) ((= n 1) 1) (else (+ (fibonacci (- n 1 (fibonacci (- n 2 (define (bar a b c) (if (= b 0) c (bar (+ a 1) (- b 1) (* a b (define (map-reduce f l op init) (reduce (map f l) op init (define (map f l) (if (null? l) () (cons (f (car l (map f (cdr l) (define (reduce l op init) (if (null? l) init (op (car l) (reduce (cdr l) op init (define (word-count pages) (map-reduce wc pages + 0 (define (make-dictionary pages) (map-reduce mw (words pages) merge ()
다음 맞는프로그램인지확인하기 1 프로그래밍기본부품과조합 (elements & compound) 2 이름짓기 (binding, delclaration, definition) 3 재귀와고차함수 (recursion & higher-order functions) 4 프로그램의계산복잡도 (program complexity) 5 타입으로정리하기 (types & typeful programming) 6 맞는프로그램인지확인하기 (program correctness) 프로그램을돌리기전에 (static test) 분석검증후프로그램제출 / 출시 / 탑재 다른공학분야와동일 : 기계 / 전기 / 공정 / 건축설계분석검증후제작 / 설비 / 건설 일상과동일 : 입시 / 면접, 사주 / 궁합, 클럽기도검증후실행 4190.210 에서는간단한기술만 확인 : 모든입력에대해서정의되었는가? 검증해야할성질들 제대로생겼는가? 자동검증 타입에맞게실행될것인가? 직접검증 (Scheme, C, JavaScript, etc) 자동검증 (ML, Scala, Haskell, Java, Python, etc) 4190.210: 모든입력에대해서정의되었는가? 직접검증, 용이 4190.210: 항상끝나는가 : 직접검증, 비교적용이 타입에맞게실행될것이확인된경우 타입에맞게실행될것이확인안된경우 데이터구현을익히고나서. 내가바라는계산을하는가 : 어려움
확인 : 항상끝나는가? 끝나는재귀함수인지확인하기 그렇다, 만일 : 반복될때뭔가가계속 줄어들고 그줄어듬의 끝이있다 면. 즉, 재귀함수의경우, 만일 : 재귀호출마다인자가 줄어들고 그줄어듬의 끝이있다 면. (define (fac n) (if (= n 0) 1 (* n (fac (- n 1) 음이아닌정수만입력으로받는다면, 재귀호출마다원래 n보다줄고있고 n-1, 끝이있다 ( (= n 0) 1 ). 끝나는재귀함수인지확인하기 일반방법 : 끝나는재귀함수인지확인하기 아래와같은재귀함수 f : A B 를생각하자 (w.l.o.g.) (define (fibonacci n) (cond ((= n 0) 0) ((= n 1) 1) (else (+ (fibonacci (- n 1 (fibonacci (- n 2 (define (f x) (f e 1 ) (f e 2 ) ) 재귀함수인자들의집합 A에서 원소들간의줄어드는순서 > 를찾으라, 아래와같은 : 재귀호출인자식 (e 1 와 e 2 ) 의값이원래인자 (x) 보다 > 인 ( 줄어드는 ), 그리고 집합 A에서 >-순서대로원소를줄세우면항상유한한 (finitely well-founded).
끝나는재귀함수인지확인하기 (define (bar a b c) (if (= b 0) c (bar (+ a 1) (- b 1) (* a b N N N 에서줄어드는순서 > 는? 그래서그 >- 순서가항상유한번에바닥에 닿는 (finitely well-founded)? 그런순서 > 는? 끝나는재귀함수인지확인하기 (define (map-reduce f l op init) (reduce (map f l) op init (define (map f l) (if (null? l) () (cons (f (car l (map f (cdr l) (define (reduce l op init) (if (null? l) init (op (car l) (reduce (cdr l) op init (define (word-count pages) (map-reduce wc pages + 0 (define (make-dictionary pages) (map-reduce mw (words pages) merge () 끝나는재귀함수인지확인하기 끝나는재귀함수인지확인하기 (define (sum lower upper f) (if (> lower upper) 0 (+ (f lower) (sum (+ lower 1) upper f (define (sigma lower upper) (lambda (f) (define (loop n) (if (> n upper) 0 (+ (f n) (loop (+ n 1) (loop upper)
끝나는재귀함수인지확인하기 f(ɛ, c) = f(c, c) = (c c ) f(c, c) = {ɛ} f(r 1 r 2, c) = f(r 1, c) f(r 2, c) f(r, c) = {r r r f(r, c)} f(cr 2, c) = {r 2 } f(c r 2, c) = (c c ) f(ɛr 2, c) = f(r 2, c) f((r 11 r 12 )r 2, c) = f(r 11 (r 12 r 2 ), c) f((r 11 r 12 )r 2, c) = f(r 11 r 2, c) f(r 12 r 2, c) f(r1r 2, c) = f(r 2, c) {r r1r 2 r f(r 1, c)}