Agda의 평가 전략은 어디에서 지정 되었습니까?

Question

모든 Agda 프로그램이 종료되었다는 것을 감안할 때, 평가 전략은 의미 론적 의미에 대해서는 중요하지 않지만 성능면에서 중요합니다 (Agda 프로그램을 실행하는 경우).

그래서 Agda는 어떤 평가 전략을 사용합니까? 데이터 변경 평가 전략 대신 코다 데이터 (♯, ♭)를 사용합니까? 게으른 평가라고하는 호출을 필요로하는 방법을 강요하는 방법이 있습니까?

Answer 1

유형 검사를 수행하려면 일반 형식으로 평가해야 할 수 있으므로 프로그램을 실행하지 않아도 문제가 발생합니다 (유형 검사 중 평가는 프로그램 실행으로 간주 될 수 있음). Agda는 정상적인 순서로 표현식을 평가합니다. 즉, 인수가 평가되기 전에 함수가 적용됩니다. 데이터 유형은 필요시에만 평가됩니다.

예를 들어, 내가 그들에 자연수 일부 조작의 정의가 있다고 가정

data ℕ : Set where 
    zero : ℕ 
    suc : ℕ → ℕ 

{-# BUILTIN NATURAL ℕ #-} 
-- Older Agda versions might require you to specify 
-- what is zero and what is suc. 

infixl 4 _+_ 
infixl 5 _*_ 
infixr 6 _^_ 

_+_ : (m n : ℕ) → ℕ 
zero + n = n 
suc m + n = suc (m + n) 

_*_ : (m n : ℕ) → ℕ 
zero * n = zero 
suc m * n = n + m * n 

_^_ : (m n : ℕ) → ℕ 
m^zero = suc zero 
m^suc n = m * m^n 

을 우리는 상당한 시간이 걸릴 것 2^16을 평가, 단항 숫자로 작업하기 때문에. 그러나 const 1 (2^16)을 평가하려고하면 거의 시간이 끝나지 않을 것입니다.

const : ∀ {a b} {A : Set a} {B : Set b} → 
    A → B → A 
const x _ = x 

같은 일이 데이터 유형에 간다 :

infixr 3 _∷_ 

data List {a} (A : Set a) : Set a where 
    [] : List A 
    _∷_ : A → List A → List A 

record ⊤ {ℓ} : Set ℓ where 

Head : ∀ {a} {A : Set a} → List A → Set _ 
Head   []  = ⊤ 
Head {A = A} (_ ∷ _) = A 

head : ∀ {a} {A : Set a} (xs : List A) → Head xs 
head []  = _ 
head (x ∷ _) = x 

replicate : ∀ {a} {A : Set a} → ℕ → A → List A 
replicate 0  _ = [] 
replicate (suc n) x = x ∷ replicate n x 

다시 head (replicate 1000000 1) 거의 즉각적으로 평가합니다.

그러나 정상적인 순서는 call-by-need, 즉 계산이 공유되지 않습니다.

open import Data.Product 
open import Relation.Binary.PropositionalEquality 

slow : 2^16 ≡ 65536 
slow = refl 

slower₁ : (λ x → x , x) (2^16) ≡ (65536 , 65536) 
slower₁ = refl 

slower₂ : 
    let x : ℕ 
     x = 2^16 
    in _≡_ {A = ℕ × ℕ} (x , x) (65536 , 65536) 
slower₂ = refl 

이 경우, 두 배의 시간을 대략 slow 요구를 취할 것 slower₁ 및 slower₂를 확인 입력합니다. 이와 비교하여 통화 별은 x의 계산을 공유하고 2^16을 한 번만 계산합니다.

---

형식 검사 중에 일반 형식으로 식을 평가해야합니다. 주변에 바인더가있는 경우 (λ 또는 Π), 바인더 아래로 가서 내부 표현식을 평가해야합니다.

λ n → 1 + n ==> λ n → suc n 

---

어떻게 사진을 변경 CODATA합니까? 환원과의 상호 작용은 실제로 매우 간단합니다. ♭을 적용하지 않으면 ♯ x은 더 이상 평가하지 않습니다. 이 ♯ 지연과 같은 힘 ♭ 알려진 이유

이

도이다.

---

또한 Agda를 Haskell로 컴파일 할 수도 있습니다. 자바 스크립트도 있지만 컴파일 된 방법을 모르겠습니다. 그래서 Haskell에게 편집을 맡깁니다.

평가 전략은 주로 하스켈 컴파일러가 사용하는 모든 것입니다.예를 들어, 여기에 다음과 같은 정의에 일어나는 내용은 다음과 같습니다

data ℕ : Set where 
    zero : ℕ 
    suc : ℕ → ℕ 

_+_ : (m n : ℕ) → ℕ 
zero + n = n 
suc m + n = suc (m + n) 

data Vec {a} (A : Set a) : ℕ → Set a where 
    [] : Vec A zero 
    _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) 

그리고 컴파일 후를 :

-- ℕ 
data T1 a0 = C2 
      | C3 a0 

-- Vec 
data T12 a0 a1 a2 = C15 
        | C17 a0 a1 a2 

-- _+_ 
d6 (C2) v0 = MAlonzo.RTE.mazCoerce v0 
d6 v0 v1 
    = MAlonzo.RTE.mazCoerce 
     (d_1_6 (MAlonzo.RTE.mazCoerce v0) (MAlonzo.RTE.mazCoerce v1)) 
    where d_1_6 (C3 v0) v1 
     = MAlonzo.RTE.mazCoerce 
      (C3 
      (MAlonzo.RTE.mazCoerce 
       (d6 (MAlonzo.RTE.mazCoerce v0) (MAlonzo.RTE.mazCoerce v1)))) 

그래가, 마지막 하나는 약간 미친 짓이야. 그러나 조금 멍청한 사람이라면 다음을 볼 수 있습니다.

d6 C2 v0 = v0 
d6 (C3 v0) v1 = C3 (d6 v0 v1)