함수 프로그래밍이 "수학적"으로 간주됩니까? 그렇다면 왜?

Question

가끔씩 "함수형 프로그래밍 언어가 더 수학적"이라고 말하는 사람이 있습니다. 그렇지? 그렇다면 왜, 어떻게? 예를 들어 Scheme은 Java 또는 C보다 수학적입니까? 아니면 하스켈?

나는 "수학적"인 것을 정확히 정의 할 수는 없지만, 당신이 그 느낌을 얻을 수 있다고 믿습니다.

감사합니다.

Answer 1

models of computation : Lambda Calculus (LC) 모델과 Turing Machine (TM) 모델은 두 가지 공통적 인 (*) models of computation입니다.

람다 미적분은 유형의 도메인에 대한 함수 구성을 통해 결과가 산출되는 수학적 형식을 사용하여 계산에 접근합니다. LC는 또한 Combinatory Logic과 관련이 있으며, 동일한 주제에 대해보다 일반적인 접근 방식으로 간주됩니다.

튜링 기계 모델은 기본 조작 (덧셈, 돌연변이 등)을 사용하여 이상화 된 저장소에 저장된 기호를 조작하여 표현하는 방식으로 계산에 접근합니다.

이러한 다양한 계산 모델은 다양한 프로그래밍 언어 제품군의 기초입니다.람다 미적분은 ML, Scheme 및 Haskell과 같은 언어를 발생 시켰습니다. 튜링 모델은 C, C++, Pascal 등으로 증가했습니다. 일반화로서, 대부분 functional programming 언어는 람다 미적분학에 이론적 근거를 가지고 있습니다.

람다 미적분의 특성상, 원칙에 따라 구축 된 시스템의 동작에 대한 확실한 증명이 가능합니다. 실제로, 증명 가능성 (예 : correctness)은 LC에서 중요한 개념이며 LC 시스템에 대한 특정 종류의 추론 및 결론을 가능하게합니다. LC는 유형 이론 및 범주 이론과도 관련이 있습니다.

대조적으로 Turing 모델은 형식 이론에 의존하지 않으며 기본 모델에서 일련의 상태 변환으로 계산을 구성하는 데 더 많이 사용됩니다. Turing Machine 계산 모델은 LC 기반 프로그램이 수행하는 것과 동일한 종류의 수학적 교정 및 조작에 대한 주장을하기가 더 어렵습니다. 그러나 이것이 TM 모델의 일부 중요한 측면은 프로그램의 가상화 및 정적 분석을 연구 할 때 사용된다는 분석은 불가능하다는 것을 의미하지는 않습니다.

함수형 프로그래밍은 유형을 신중하게 선택하고 유형 간 변환을 사용하기 때문에 FP는 더 "수학적"이라고 인식 될 수 있습니다.

(*) 다른 계산 모델도 있지만이 토론과는 관련성이 낮습니다.

Answer 2

순수한 함수형 언어는 부작용이 없다는 것, 즉 변경할 수있는 상태가 없다는 것, 입력 매개 변수 만 결과 값에 매핑한다는 것입니다. 이는 수학 함수가하는 것입니다.

Answer 3

함수 프로그래밍의 논리 구조는 크게 based on lambda calculus입니다. 대수적 형태의 수학에만 기초한 것으로 보이지는 않지만 very easily from discrete mathematics이라고 쓰여 있습니다.

명령형 프로그래밍과 비교할 때, 뭔가를하는 방법을 정확히 규정하지는 않지만 반드시 수행해야 할 작업이 있습니다. 이것은 토폴로지를 반영합니다.

Answer 4

함수 프로그래밍 언어의 수학적 느낌은 몇 가지 다른 기능에서 비롯됩니다. 가장 명백한 것은 이름입니다. "기능적", 즉 수학에 기본이되는 기능을 사용합니다. 다른 중요한 이유는 함수 프로그래밍이 상호 작용에 의해 원하는 계산을 달성하는 사실의 컬렉션을 정의하는 것입니다. 이것은 수학적 증명이 수행되는 것과 유사합니다.

Answer 5

순수 함수 프로그래밍 언어는 functional calculus의 예이므로 이론적으로 함수 언어로 작성된 프로그램은 수학적으로 추론 할 수 있습니다. 이상적으로 당신은 프로그램이 정확하다는 것을 '증명할'수 있기를 원합니다.

실제로 이러한 추론은 사소한 경우를 제외하고는 매우 어렵지만 어느 정도 가능합니다. 프로그램의 특정 속성을 증명할 수 있습니다. 예를 들어 프로그램에 대한 모든 숫자 입력이 주어진 경우 출력이 항상 특정 범위 내로 제한된다는 것을 증명할 수 있습니다.

변경 가능한 상태와 부작용이있는 비 기능적 언어에서 프로그램에 대한 추론을 시도하고 '정확함'을 증명하려고 시도하는 것은 거의 불가능합니다. 비 기능적 프로그램을 사용하면 프로그램을 통해 생각해 볼 수 있으며 그 부분이 정확하다는 것을 확신 할 수 있으며 특정 입력을 테스트하는 단위 테스트를 실행할 수 있지만 일반적으로 프로그램 동작에 대한 엄격한 수학적 증명을 구축 할 수는 없습니다.