Safe Agda

Safe Agda

--safe 옵션(프래그마 옵션 또는 명령줄로)을 사용하면, Agda가 불일치(inconsistency)로 이어질 수 있는 기능들이 비활성화되도록 보장하게 할 수 있어요.

다음은 --safe와 호환되지 않는 기능 목록이에요:

  • postulate; 임의의 공리를 가정하는 데 사용할 수 있어요.
  • --allow-unsolved-metas; Agda가 끝나지 않은 증명을 받아들이도록 강제해요.
  • --allow-incomplete-matches와 NON_COVERING 프래그마; 부분 함수나 부분 증명을 통해 거짓을 증명할 수 있게 해요.
  • --no-positivity-check와 NO_POSITIVITY_CHECK, POLARITY 프래그마; 엄격하게 양(positive)이 아닌 데이터 타입을 통해 비종료 프로그램을 작성할 수 있게 해요.
  • --no-termination-check와 TERMINATING, NON_TERMINATING 프래그마; 루프 프로그램에 임의의 타입을 주게 해요.
  • --type-in-type, --omega-in-omega와 NO_UNIVERSE_CHECK 프래그마; 사용자가 Girard-Hurken 역설을 인코딩할 수 있게 해요.
  • INJECTIVE 프래그마; 주입적이지 않은 함수를 주입적이라고 선언해 거짓을 증명할 수 있게 해요.
  • --injective-type-constructors; 배중률(excluded middle)과 함께하면 Chung-Kil Hur의 구성으로 불일치로 이어져요.
  • --sized-types; 크기의 부적절하고 불일치적인 사용을 배제하는 일부 검사가 없어요.
  • --experimental-irrelevance와 --irrelevant-projections; 잠재적으로 불건전한 비관련성(irrelevance) 기능을 활성화해요 (각각 비관련 레벨, 비관련 데이터 매칭, 비관련 레코드 필드의 projection).
  • --rewriting; 어떤 방정식이든 정의적으로 성립(definitionally)하게 바꿔요. 적어도 수렴(convergence)을 깨뜨릴 수 있어요.
  • --cubical=compatible를 --with-K와 함께; 큐빅 구성으로 유니벌런스 공리를 증명할 수 있는데, 이는 K 공리를 부정해요.
  • --without-K를 --flat-split과 함께.
  • primEraseEquality 프리미티브를 --without-K와 함께; primEraseEquality를 사용하면 K 공리를 유도할 수 있어요.
  • --allow-exec; 타입 체킹 중 시스템 호출을 허용해요.
  • --no-load-primitives; 사용자가 sort와 level 프리미티브를 수동으로 바인딩하게 해요.
  • --cumulativity; 유니버스 레벨 해결을 위한 열악한 휴리스틱 때문이에요.
  • --large-indices를 --without-K 또는 --forced-argument-recursion과 함께; 이 두 조합 모두 불일치적인 것으로 알려져 있어요.
  • COMPILE 프래그마; 컴파일 중 코드의 의미를 바꿀 수 있게 해요.

--safe 옵션은 감염성(coinfective)이에요 (일관성을 위한 옵션 검사 참고); 모듈이 안전으로 선언되면, 그 모듈이 임포트한 모든 모듈도 안전으로 선언되어야 해요.

더 알아보기 (Learn more)