전체 함수형 프로그래밍

전체 함수형 프로그래밍(, 일반적인 또는 약한 함수형 프로그래밍과 대조하여 강한 함수형 프로그래밍(strong functional programming)이라고도 함This term is due to: .)은 프로그램의 범위를 증명 가능하게 종료되는 프로그램으로만 제한하는 프로그래밍 패러다임이다.

 제한 사항 
종료는 다음과 같은 제한 사항에 의해 보장된다.

 월터 재귀(Walther recursion), 부분구조 재귀(substructural recursion) 또는 코드의 추상 해석에 의해 입증된 "강한 정규화"와 같이 인수의 '축소된' 형태에서만 작동하는 제한된 형태의 재귀.
 모든 함수는 (부분 정의 함수와 대조되는) 전체 함수여야 한다. 즉, 도메인 내부의 모든 것에 대해 정의가 있어야 한다.
 나눗셈과 같이 흔히 사용되는 부분 함수를 전체 함수로 확장하는 몇 가지 가능한 방법이 있다. 함수가 일반적으로 정의되지 않는 입력에 대해 임의의 결과를 선택하거나(예를 들어 나눗셈의 경우 ), 해당 입력에 대한 결과를 지정하기 위해 다른 인수를 추가하거나, 정제형(refinement types)과 같은 타입 시스템 기능을 사용하여 이를 제외하는 방법이 있다.

이러한 제한은 전체 함수형 프로그래밍이 튜링 완전(Turing-complete)하지 않음을 의미한다. 그러나 사용할 수 있는 알고리즘의 집합은 여전히 방대하다. 예를 들어, (그 자체로 월터 재귀만 사용하는 프로그램에 의해) 점근적 상한을 계산할 수 있는 모든 알고리즘은, 매 반복이나 재귀마다 감소하는 추가 인수로 상한을 사용함으로써 증명 가능하게 종료되는 함수로 사소하게 변환될 수 있다.

예를 들어, 퀵 정렬은 부분구조 재귀임을 사소하게 보여줄 수는 없지만, 최대 벡터 길이의 깊이까지만 재귀한다(최악의 경우 시간 복잡도 O(n2)). 리스트에 대한 퀵 정렬 구현(부분구조 재귀 검사기에 의해 거부될 수 있음)을  하스켈을 사용하여 작성하면 다음과 같다.
import Data.List (partition)

qsort []       = []
qsort [a]      = [a]
qsort (a:as)   = let (lesser, greater) = partition (<a) as
                 in qsort lesser ++ [a] ++ qsort greater

벡터의 길이를 제한으로 사용하여 부분구조 재귀로 만들려면 다음과 같이 할 수 있다.
import Data.List (partition)

qsort x = qsortSub x x
-- 최소 케이스
qsortSub []     as     = as -- 종료를 보여줌
-- 표준 qsort 케이스
qsortSub (l:ls) []     = [] -- 재귀적이지 않으므로 허용됨
qsortSub (l:ls) [a]    = [a] -- 재귀적이지 않으므로 허용됨
qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as
                            -- 재귀적이지만, 첫 번째 입력의 부분구조인 ls에 대해
                            -- 재귀를 수행함.
                         in qsortSub ls lesser ++ [a] ++ qsortSub ls greater

일부 알고리즘 클래스는 이론적인 상한은 없지만 실질적인 상한을 갖기도 한다(예를 들어, 일부 휴리스틱 기반 알고리즘은 일정 횟수의 재귀 후에 "포기"하도록 프로그래밍하여 종료를 보장할 수 있다).

전체 함수형 프로그래밍의 또 다른 결과는 원칙적으로 엄격한 계산법과 느긋한 계산법이 모두 동일한 동작을 초래한다는 것이다. 그러나 성능상의 이유로 한 쪽이 여전히 선호될 수(또는 요구될 수) 있다.The differences between lazy and eager evaluation are discussed in:  See in particular pp. 86–91.

전체 함수형 프로그래밍에서는 자료와 공자료(codata)를 구분한다. 전자는 유한하고 후자는 잠재적으로 무한하다. 이러한 잠재적으로 무한한 데이터 구조는 I/O와 같은 애플리케이션에 사용된다. 공자료를 사용하는 것은 공재귀(corecursion)와 같은 연산의 사용을 수반한다. 그러나 공자료 없이도 (의존형을 사용하는) 전체 함수형 프로그래밍 언어에서 I/O를 수행하는 것이 가능하다. Archived copy

에피그램과 차리티는 데이비드 터너가 논문에서 명시한 방식과 다르게 작동하더라도 전체 함수형 프로그래밍 언어로 간주될 수 있다. 순수한 시스템 F, 마틴-뢰프 타입 이론 또는 구성의 계산법에서 직접 프로그래밍하는 것도 마찬가지이다.

 같이 보기 
 정지 분석

 각주 

분류:함수형 프로그래밍
분류:프로그래밍 패러다임