Agda

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 특징
3. 역사
참조

1. 개요

Agda는 찰머스 공과대학교에서 개발된 의존형 이론 기반의 증명 지원 시스템이자 프로그래밍 언어이다. 유도 자료형, 종속 타입 패턴 매칭, 메타변수, 증명 자동화, 종료 검사 등의 특징을 가지며, 유니코드와 표준 라이브러리를 광범위하게 사용한다. Haskell과 JavaScript를 위한 두 개의 컴파일러 백엔드를 제공하며, Agda 2는 Ulf Norell에 의해 개발이 이어지고 있다.

더 읽어볼만한 페이지

2007년 개발된 프로그래밍 언어 - 클로저 (프로그래밍 언어)
클로저는 리치 히키가 개발한 JVM 기반의 함수형 프로그래밍 언어로, 자바와의 호환성을 특징으로 하며 불변 데이터 구조와 STM을 활용한 동시성 관리, 그리고 REPL 환경, 매크로 시스템 등의 기능을 제공한다.
2007년 개발된 프로그래밍 언어 - Nu (프로그래밍 언어)
Nu는 Objective-C, Lisp, 루비의 영향을 받아 설계되었으며, 한국 소프트웨어 산업의 혁신에 기여할 잠재력을 가진 프로그래밍 언어이다.
패턴 매칭 프로그래밍 언어 - AWK
AWK는 1977년에 개발된 텍스트 처리 및 프로그래밍 언어로, 유닉스 환경에서 텍스트 처리를 위해 설계되었으며 정규 표현식 처리 기능을 통해 텍스트 분석, 데이터 추출, 보고서 생성 등 다양한 작업을 수행한다.
패턴 매칭 프로그래밍 언어 - 하스켈
하스켈은 해스켈 커리의 이름을 딴 순수 함수형 프로그래밍 언어로, 여러 함수형 언어 통합 노력의 결과로 탄생하여 느긋한 계산법, 패턴 매칭, 타입 클래스, 모나드 등의 특징을 가지며 GHC가 표준 구현체로 사용된다.

Agda - [IT 관련 정보]에 관한 문서
개요
아그다 공식 로고
패러다임	함수형
디자이너	울프 노렐; 카타리나 코캉 (1.0)
개발자	찰머스 공과대학교
최초 출시	1.0 – 1999년
안정화 버전 출시	2.7.0
안정화 버전 출시일	2024년 8월 16일
타이핑	강한, 정적, 종속, 명목적, 명시적, 추론
구현체	해당 사항 없음
영향을 준 언어	이드리스
영향을 받은 언어	Coq, Epigram, Haskell
라이선스	BSD와 유사
파일 확장자	.agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
운영 체제	크로스 플랫폼
웹사이트	아그다 위키
기타 정보
종류	(증명 지원 시스템)
영향을 받은 언어	Coq, (Epigram, ML, Haskell)

2. 특징

Agda는 찰머스 공과대학교에서 개발되던 의존형 이론 기반 증명 지원 시스템(ALF, Alfa)과 프로그래밍 언어(Cayenne)에 이어 개발되었다. 2000년대 중반 Agda2로 대폭 개량되었으며(이전 버전은 Agda1로 표기), Ulf Norell에 의해 찰머스에서 개발이 계속되고 있다. Agda2는 구문이 변경되었고(변환 도구 존재), 유니코드를 널리 사용하여 가독성이 높은 증명을 얻을 수 있다.^[1]

Makoto Takeyama와 Nils Anders Danielsson이 개발한 명령줄 도구와 Emacs 모드를 제공한다. Agda 구현자 회의(AIM)가 정기적으로 개최되며, Code Sprint라는 공동 작업을 통해 기능 확장, 문서 정비, 라이브러리 작성 등이 이루어진다.

Agda는 Epigram과 유사하며, 유도 자료형, 종속 타입 패턴 매칭, 메타변수, 증명 자동화, 종료 검사, 표준 라이브러리, 유니코드 지원, 하스켈, 자바스크립트 백엔드 등의 특징을 가진다.

2. 1. 유도 자료형 (Inductive types)

Agda에서 자료형을 정의하는 주요 방법은 대수적 자료형과 유사한 유도 자료형을 이용하는 것이다.

다음은 Agda에서 페아노 수를 정의하는 예시이다.

```agda

data ℕ : Set where

zero : ℕ

suc : ℕ → ℕ

```

기본적으로, 이는 자연수를 나타내는

\mathbb{N}

형식의 값을 구성하는 두 가지 방법이 있음을 의미한다. 먼저, `zero`는 자연수이고, `n`이 자연수이면 `n`의 후속자를 나타내는 `suc n`도 자연수이다.

다음은 두 자연수 사이의 "작거나 같음" 관계를 정의하는 예시이다.

```agda

data _≤_ : ℕ → ℕ → Set where

z≤n : {n : ℕ} → zero ≤ n

s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

```

첫 번째 생성자 `z≤n`은 0이 모든 자연수보다 작거나 같다는 공리에 해당한다. 두 번째 생성자 `s≤s`는 `n ≤ m`의 증명을 `suc n ≤ suc m`의 증명으로 바꾸는 것을 허용하는 추론 규칙에 해당한다.^[9] 따라서 `s≤s {zero} {suc zero} (z≤n {suc zero})` 값은 1(0의 후속자)이 2(1의 후속자)보다 작거나 같다는 증명이다. 중괄호로 제공된 매개변수는 추론할 수 있는 경우 생략할 수 있다.

2. 2. 종속 타입 패턴 매칭 (Dependently typed pattern matching)

Agda는 귀납적 타입에 대한 정리를 증명하기 위해 종속 타입 패턴 매칭을 사용한다. 이는 핵심 타입 이론에서 귀납 및 재귀 원리를 사용하는 것보다 자연스러운 방식으로 재귀 함수/귀납적 증명을 작성할 수 있게 한다.^[1] 예를 들어 자연수 덧셈은 다음과 같이 정의할 수 있다.^[1]

```agda

add zero n = n

add (suc m) n = suc (add m n)

```

Agda에서 종속 타입 패턴 매칭은 언어의 기본 요소이다. 핵심 언어에는 패턴 매칭으로 변환되는 귀납/재귀 원리가 없다.^[1]

2. 3. 메타변수 (Metavariables)

Agda는 Coq와 같은 다른 유사한 시스템에 비해 프로그램 구성에 메타변수를 적극적으로 활용한다. 예를 들어, Agda에서 다음과 같이 함수를 작성할 수 있다.

```agda

add : ℕ → ℕ → ℕ

add x y = ?

```

여기서 `?`는 메타변수이다. Emacs 모드에서 시스템과 상호 작용할 때, 예상되는 유형을 사용자에게 보여주고 메타변수를 구체화할 수 있도록 한다. 즉, 더 자세한 코드로 대체할 수 있다. 이 기능은 Coq와 같은 전술 기반 증명 보조자와 유사한 방식으로 점진적인 프로그램 구성을 가능하게 한다.^[1]

2. 4. 증명 자동화 (Proof automation)

Agda는 별도의 택틱 언어 없이도 Agda 내에서 유용한 택틱을 프로그래밍할 수 있도록 한다. 이는 관심 있는 속성에 대한 증명을 선택적으로 반환하는 Agda 함수를 작성하여 구현한다. 예를 들어, 숫자를 입력받아 짝수임을 증명하는 함수를 작성하고, 타입 검사 시간에 이 함수를 실행하여 택틱을 구성할 수 있다.^[10]

반사 프로그래밍(reflection)을 통한 자동화를 지원하며, 이를 통해 프로그램 조각을 추상 구문 트리로 인용하거나 인용 해제할 수 있다. 이는 템플릿 하스켈(Template Haskell)과 유사하게 작동한다.^[10]

Emacs 모드에서의 증명 검색 액션을 통해 가능한 증명 항을 열거하고, 사양에 맞는 항을 메타 변수에 넣을 수 있다. 이 액션은 어떤 정리와 모듈을 사용할지, 패턴 매칭을 사용할지 등 힌트를 제공하여 검색을 돕는다.^[11]

2. 5. 종료 검사 (Termination checking)

Agda는 전체 함수형 프로그래밍 언어이다. 즉, 모든 프로그램은 종료되어야 하며 모든 가능한 패턴이 일치해야 한다.^[12] 이 기능이 없으면 언어의 논리가 일관성을 잃고 임의의 명제를 증명하는 것이 가능해진다. 종료 검사를 위해 Agda는 Foetus 종료 검사기 방식을 사용한다.^[12]

2. 6. 표준 라이브러리 (Standard library)

Agda는 광범위한 사실상의 표준 라이브러리를 가지고 있으며, 여기에는 자연수, 리스트, 벡터와 같은 기본적인 데이터 구조에 대한 유용한 정의와 정리가 많이 포함되어 있다. 이 라이브러리는 베타 버전이며 활발하게 개발되고 있다.

2. 7. 유니코드 (Unicode)

Agda는 프로그램 소스 코드에서 유니코드를 광범위하게 사용하는 것이 특징이다. 표준 emacs 모드는 `\Sigma`를 Σ로 입력하는 단축키를 제공한다.

2. 8. 백엔드 (Backends)

Agda는 두 개의 컴파일러 백엔드를 가지고 있는데, 하나는 하스켈용 MAlonzo이고 다른 하나는 자바스크립트용이다.

3. 역사

Agda는 당시 찰머스 공과대학교에서 개발되던 의존형 이론 기반 증명 지원 시스템(ALF, Alfa)과 프로그래밍 언어(Cayenne)에 이어 개발되었다. 2000년대 중반에 대폭적인 개량이 계획되어, Agda2로 구현되었다(이전 버전을 Agda1로 표기하여 구분하는 경우도 많다). Agda2는 Ulf Norell에 의해 찰머스에서 개발이 계속되고 있다. 인스턴스 유도, 문맥에서 추론할 수 있을 때는 생략할 수 있는 암묵적 변수 등, 구문은 Agda 1에서 변경되었다(단, 변환 도구가 개발되고 있다). Agda 2는 더욱 가독성이 높은 증명을 얻기 위한 방법으로, 유니코드가 널리 사용되고 있다.

Agda 2는 Makoto Takeyama와 Nils Anders Danielsson에 의해 개발된 명령줄 도구 및 강력한 Emacs 모드를 모두 제공한다.

Agda 구현자 회의(AIM: Agda Implementers' Meeting)가 정기적으로 개최되고 있다. 회의 기간 중 Code Sprint라고 불리는 공동 작업에 많은 시간이 할당되며, 참가자는 소그룹으로 나뉘어 Agda의 기능 확장, 문서 정비, 라이브러리 작성 등을 진행한다.

Agda 2는 Epigram과 유사하다.

참조

_[1] 문서 Agda license file http://code.haskell.[...]
_[2] 논문 Towards a practical programming language based on dependent type theory http://www.cse.chalm[...] Chalmers University of Technology 2007
_[3] 웹사이트 Agda: An Interactive Proof Editor https://web.archive.[...] 2014-10-20
_[4] 간행물 An Emacs interface for type directed support constructing proofs and programs https://web.archive.[...] 2005
_[5] 웹사이트 agda-mode on Atom https://atom.io/pack[...] 2017-04-07
_[6] 웹사이트 agda-mode - Visual Studio Marketplace https://marketplace.[...] 2023-06-06
_[7] 서적 Computation and reasoning: a type theory for computer science Oxford University Press, Inc. 1994
_[8] 웹사이트 "[Agda] origin of \"Agda\"? (Agda mailing list)" https://lists.chalme[...] 2020-10-24
_[9] 웹사이트 Nat from Agda standard library https://github.com/a[...] 2014-07-20
_[10] 간행물 "Engineering proof by reflection in Agda." http://hal.inria.fr/[...] Springer Berlin Heidelberg 2013
_[11] 문서 Auto in Agda http://www.staff.sci[...]
_[12] 간행물 "foetus – Termination checker for simple functional programs." http://www.tcs.infor[...] 1998
_[13] 웹사이트 Release notes for Agda version 2.6.4.3 https://hackage.hask[...] 2024-06-02
_[14] 문서 Agda license file http://code.haskell.[...]
_[15] 논문 Towards a practical programming language based on dependent type theory Chalmers University of Technology 2007
_[16] 웹인용 Agda: An Interactive Proof Editor https://web.archive.[...] 2014-10-20
_[17] 간행물 An Emacs interface for type directed support constructing proofs and programs https://web.archive.[...]
_[18] 웹인용 agda-mode on Atom https://atom.io/pack[...] 2017-04-07
_[19] 서적 Computation and reasoning: a type theory for computer science Oxford University Press, Inc. 1994

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com