아그다(프로그래밍 언어)

아그다

패러다임	기능하다
설계자	울프 노렐; 카타리나 코칸드 (1.0)
개발자	울프 노렐; 카타리나 코칸드 (1.0)
처음 등장한	2007년, 15년 전(2007년)(1999년 1.0, 23년 전(1999년))
안정된 릴리스	2.6.2 / 2021년 6월 19일, 13개월 전(2021-06-19)
타이핑 분야	strong, static, dependent, nominal, 매니페스트, 추론
구현 언어	하스켈
OS	크로스 플랫폼
면허증.	BSD와 같은[1]
파일 이름 확장자	.agda,.lagda,.lagda.md,.lagda.rst,.lagda.tex
웹 사이트	wiki.portal.chalmers.se/agda
영향을 받다
Coq, 에피그램, 하스켈
영향받은
이드리스

Agda는 Chalmers University of Technology의 Ulf Norell에 의해 개발된 의존형 함수 프로그래밍 언어이며, 그의 ^[2]박사논문에 기술되어 있습니다.최초의 아그다 시스템은 1999년 ^[3]Catarina Coquand에 의해 Chalmers에서 개발되었다.원래 아그다 2로 알려진 현재의 버전은 완전한 개서이며, 이름과 전통을 공유하는 새로운 언어로 간주되어야 한다.

아그다 역시 Propositions-as-type 패러다임을 기반으로 한 증명 도우미이지만 Coq와 달리 별도의 전술 언어가 없으며 증명은 함수 프로그래밍 스타일로 작성됩니다.이 언어는 데이터 유형, 패턴 매칭, 레코드, 렛 식과 모듈, 하스켈과 같은 구문과 같은 일반적인 프로그래밍 구조를 가지고 있습니다.시스템에는 Emacs 및 ATOM 인터페이스가^[4][5] 있지만 명령줄에서 배치 모드로 실행할 수도 있습니다.

아그다는 마틴-뢰프 유형 이론과 유사한 유형 이론인 Zhaohui Luo의 UTT에 기초하고 있습니다.^[6]

아그다의 이름은 스웨덴 노래 "회난 아그다"에서 따왔다. 이 노래는 코넬리스 브레스베이크가 ^[7]쓴 것으로, 아그다라는 이름의 암탉에 관한 것이다.이것은 Coq의 이름을 암시한다.

특징들

유도형

Agda에서 데이터 유형을 정의하는 주요 방법은 비의존형 프로그래밍 언어의 대수적 데이터 유형과 유사한 유도 데이터 유형을 사용하는 것입니다.

다음은 아그다의 Peano 번호에 대한 정의입니다.

 data : : 0 : suc suc : ℕ → zero 으로 설정합니다.

기본적으로 자연수를 나타내는 $유형{\displaystyle \mathbb{}}$ N$(\$의 값을 구성하는 방법은 두 가지가 있습니다.먼저,zero자연수이고, 만약n그럼 자연수입니다.suc n(의 후계자를 나타냄)n, 역시 자연수입니다.

다음은 두 자연수 사이의 "미만 또는 동일한" 관계에 대한 정의입니다.

 data _bps_ : → → 여기서 z :n : {n : ℕ}} → 0 ≤n s : {n m : ℕ } → n ≤ m → suc n m suc m 을 설정합니다.

첫 번째 컨스트럭터z≤n는 0이 자연수보다 작거나 같다는 공리에 해당합니다.두 번째 컨스트럭터는s≤s는 추론 규칙에 대응하여 증명서를 제출할 수 있습니다.n ≤ m의 증거로suc n ≤ suc m그 ^[8]가치는s≤s {zero} {suc zero} (z≤n {suc zero})는 1(제로의 후속)이 2(1의 후속)보다 작거나 같다는 증거입니다.대괄호로 둘러싸인 파라미터는 유추할 수 있는 경우 생략할 수 있습니다.

종속 유형 패턴 일치

핵심 유형 이론에서, 유도 및 재귀 원리는 유도 유형에 대한 이론을 증명하기 위해 사용됩니다.Agda에서는 의존적으로 입력된 패턴 매칭이 대신 사용됩니다.예를 들어 자연수 덧셈은 다음과 같이 정의할 수 있습니다.

 add 0 n = n add (m) n = suc (mn

이러한 재귀 함수/유도 증거를 작성하는 방법은 원시 유도 원리를 적용하는 것보다 더 자연스럽다.아그다에서는 의존적으로 유형화된 패턴 매칭은 언어의 원시적인 것으로, 핵심 언어에는 패턴 매칭이 변환되는 유도/재귀 원칙이 없습니다.

메타바러블

Coq와 같은 다른 유사한 시스템과 비교했을 때, Agda의 특징 중 하나는 프로그램 구축을 위한 메타바일러블에 대한 의존도가 높다는 것입니다.예를 들어, Agda에서는 다음과 같은 함수를 쓸 수 있습니다.

 add : ℕℕ → ℕ x add x y =?

?여기 메타바리블이 있습니다.emacs 모드에서 시스템과 대화하는 경우 사용자가 예상하는 유형이 표시되며 메타 변수 가능한 유형을 세분화할 수 있습니다. 즉, 보다 자세한 코드로 대체할 수 있습니다.이 기능을 통해 Coq와 같은 전술 기반 인증 보조와 유사한 방식으로 증분 프로그램 구축을 수행할 수 있습니다.

실증 자동화

순수 유형 이론에서의 프로그래밍은 많은 지루하고 반복적인 증거를 수반한다.아그다에는 별도의 전술 언어가 없지만 아그다 자체 내에서 유용한 전술 프로그래밍이 가능하다.일반적으로, 이것은 관심 있는 일부 재산의 증거를 선택적으로 반환하는 Agda 함수를 작성함으로써 작동한다.그런 다음 유형 검사 시간에 이 기능을 실행하여 전술이 구축됩니다. 예를 들어 다음과 같은 보조 정의를 사용합니다.

 데이터일 수 있음 (A: Set) : A → 아무것도 아닐 수 있음 : A → 데이터일 수 있음 {A : Set} : A → auto : { {x} → Just (x) 전술 : ∀ {A : Set} (x : Maybe A → Just A : X ) → Just A → Just A x

주어진 함수check-even : (n : ${\displaystyle \mathbb {N} }$) → Maybe (Even n)숫자를 입력하고 짝수 증명서를 선택적으로 반환하는 경우 다음과 같이 전술이 구성될 수 있습니다.

 check-even-lema : {n : Ω} → isJust (check-even n) → tactic (check-even n) lemma0 : even auto lemma0 : even auto lema0 : even (ch-lema 0) = check-even auto lema2 : even auto lema 2 = 체크-ven auto

각 보조개념의 실제 증빙은 유형 검사 시 자동으로 구성됩니다.전술이 실패하면 타입 체크는 실패합니다.

또한 보다 복잡한 전술을 작성하기 위해 Agda는 반사를 통한 자동화를 지원합니다.리플렉션메커니즘을 사용하면 프로그램 조각을 추상 구문 트리에 인용하거나 인용 해제할 수 있습니다.반사가 사용되는 방법은 템플릿 해스켈의 ^[9]작동 방식과 유사합니다.

증명 자동화의 또 다른 메커니즘은 emacs 모드에서의 증명 검색 액션입니다.가능한 증명 조건(5초 제한)이 열거되어 있으며, 조건 중 하나가 사양에 부합하면 액션이 호출되는 메타 변수에 추가됩니다.이 동작은 예를 들어 사용할 수 있는 정리 및 모듈, 패턴 매칭을 사용할 수 있는지 ^[10]여부 등의 힌트를 받습니다.

종료 확인

Agda는 전체 언어입니다. 즉, Agda의 각 프로그램은 종료되고 가능한 모든 패턴이 일치해야 합니다.이 기능이 없으면 언어의 논리에 일관성이 없어져 임의의 스테이트먼트를 증명할 수 있게 됩니다.종료 확인을 위해 Agda는 Foetus 종료 ^[11]검사기의 접근방식을 사용한다.

표준 라이브러리

Agda는 사실상의 광범위한 표준 라이브러리를 가지고 있으며, 여기에는 자연수, 목록 및 벡터와 같은 기본 데이터 구조에 대한 많은 유용한 정의와 이론이 포함되어 있습니다.라이브러리는 베타 버전으로 개발 중입니다.

유니코드

Agda의 가장 주목할 만한 특징 중 하나는 프로그램 소스 코드에서 유니코드에 크게 의존하는 것입니다.표준 emacs 모드에서는 입력에 다음과 같은 숏컷이 사용됩니다.\Sigmafor의 경우.

백엔드

컴파일러 백엔드는 Haskell용 MALonzo와 JavaScript용 두 가지가 있습니다.

「 」를 참조해 주세요.

• 동작
• HOL(프루프 어시스턴트)
• Idris(프로그래밍 언어)
• 이사벨(프루프 어시스턴트)

레퍼런스

추가 정보

• Bove, Ana; Dybjer, Peter; Norell, Ulf (n.d.). "Brief Overview of Agda – A Functional Language with Dependent Types" (PDF).
• Norell, Ulf; Chapman, James (n.d.). "Dependently Typed Programming in Agda" (PDF).

외부 링크

• 공식 웹사이트
• 다니엘 피블스의 5부작 YouTube 재생 목록인 아그다
• 잔혹한 [메타]Agda의 종속 유형 소개
• 아그다 튜토리얼: "이론적인 배경 없이 아그다에서 프로그래밍을 탐색한다"