2019-12-10
https://www.youtube.com/watch?v=AZ8wMIar-_c
다음으로 Andreev, Lizzy가 Cubical 타입을 Agda에 적용하는 것에 대한 이야기를 들어보겠습니다.
감사합니다.
이것은 Anders Mortberg 및 Andrea Vezzosi와의 공동 연구입니다.
먼저 디팬던트 타입 이론에서 동질성이 무엇인지 살펴보겠습니다.
우리가 이야기하고 Agda가 기반으로 하는 종류의 타입 이론에서는 하나의 동질성 개념을 갖는 경향이 있습니다.
언어의 모든 속성이 의존하는 주요 개념이며, 단일 생성자 refl을 가진 가장 좋은 유도 타입입니다.
이는 제거하기 매우 쉽습니다.
패턴 매칭이나 방정식에서 refl에 대한 경우만 제공하면 모든 것이 작동합니다.
모든 동질성 타입의 항이 닫힌 컨텍스트에서 refl로 줄어들기 때문에 프로그래밍 언어로도 작동할 수 있습니다.
즉, 멈추지 않습니다.
이러한 종류의 전송이 진행되지만 이 동질성은 아직 결정적이지 않습니다.
왜냐하면 이 설정에서 많은 것들이 방지되기 때문입니다.
대부분의 경우 증명에서 확장 방식으로 추론하고 싶어합니다.
언어가 두 항의 차이를 구별할 수 없는 한 두 항이 동일하게 동작하는 한 두 항이 동일함을 증명할 수 있기를 원합니다.
하지만 지금까지 보여드린 설정으로는 함수 확장성이나 유사성 원칙을 일부를 깨뜨리지 않고는 가질 수 없습니다.
예를 들어, 이것을 공리로 추가할 수 있지만 환원이 깨집니다.
멈추게 됩니다.
즉, 리더 모나드가 펑터가 아님을 증명하는 것과 같이 증명하고 싶은 매우 간단한 정리조차도 증명할 수 없습니다.
스트림은 언어 내부에서 정의된 대로 관찰 가능성에 따라 스트림에 대해서만 추론한다고 말하는 사용자 정의 동치 관계로 추론을 시작하지 않는 한 실제로 펑터의 구조를 추가하지 않습니다.
이러한 상황에서 Homotopy 타입 이론이 등장하여 이러한 것들을 자동으로 추가하기로 결정했습니다.
이는 타입을 공간으로, 동질성을 타입 간의 경로로 보면 더 많은 동질성을 사용할 수 있어야 한다는 아이디어에 의해 정당화됩니다.
특히 앞서 언급한 원칙은 이러한 종류의 해석으로 검증되며, 예를 들어 refl에 새로운 의미를 부여합니다.
refl은 시작점에 머무르는 경로입니다.
어디로도 가지 않는 경로입니다.
또한 이 시점에서 이전에는 필요하지 않았던 원칙, 예상치 못한 원칙도 추가합니다.
타입 간의 동질성을 구축하려는 경우 두 타입 간의 동치를 제공하면 되는 Univalence 공리가 있습니다.
또한 고차 유도 타입이라고 하는 것을 사용하여 이러한 종류의 경로, 이러한 종류의 동질성을 귀납적으로 추가하는 방법도 있습니다.
고차 유도 타입을 사용하면 대상 타입이 동질성인 생성자를 정의할 수 있습니다.
예를 들어, 고차 유도 타입을 자세히 살펴보면 리스트가 자유 모노이드임을 알고 있습니다.
또는 증명할 수 있지만 이는 정의 방식에서 명확하지 않습니다.
모노이드는 결합 법칙이 있는 이항 연산입니다.
고차 유도 타입이 없으면 실제로 공리에서 직접 이를 정의할 수 있습니다.
공리를 유도 타입으로 작성합니다.
연산, 모노이드의 단위를 작성합니다.
그리고 이제 몇 가지 법칙을 잊어버렸다는 것을 깨달았지만, 네.
모노이드의 단위, 이항 연산, 타입 A에서의 주입이 있습니다.
그리고 모노이드 인터페이스의 법칙을 원합니다.
이 경우 결합성만 적었습니다.
이 결합성은 데이터 타입의 새로운 생성자이며, 패턴 매칭을 할 때마다 결합성에 대해서도 뭔가를 해야 합니다.
이로부터 면역이 될 때 결합 법칙을 준수한다는 것을 증명하려고 합니다.
이제 모든 법칙을 추가하면 리스트를 이러한 종류의 표현의 정규형으로 볼 수 있습니다.
모든 것을 오른쪽으로 다시 결합하고 모든 단위를 끝에 놓기로 결정했습니다.
하지만 예를 들어, 이것은 이전에 표현할 수 있었던 종류의 것이지만 이러한 종류의 정규형을 수정하여 수행했습니다.
다른 방식으로 정규화하고 싶은 응용 프로그램이 있을 수 있으며, 이 표현은 그러한 종류의 일반성을 제공할 수 있습니다.
또한 이런 식으로 표현하면 자유 그룹을 만드는 것과 같은 것으로 일반화하기가 더 쉽습니다.
사전에 정규형이 무엇인지 또는 표현할 수 있는지조차 알 수 없습니다.
좋아요, 이것들은 Homotopy 타입 이론이 추가하는 것들입니다.
하지만 이것들을 어떻게 계산할지에 대해서는 아무것도 말해주지 않으며, 바로 여기에서 Cubical 타입 이론이 등장합니다.
2015년에서 2018년 사이에 개발된 Cubical 타입 이론은 타입 이론의 확장으로 Univalence와 고차 유도 타입에 계산적 내용을 부여하는 방법을 제공합니다.
타입과 공간 사이의 이러한 대응 관계를 조금 더 자세히 살펴보면서 이를 수행합니다.
동질성이 X와 Y 사이의 경로라면 Cubical 타입 이론에서 이 경로를 이러한 종류의 방식으로 표현합니다.
또는 0에서 1까지의 구간에서 타입 A까지의 맵으로 표현합니다.
이를 위해 이론 내부에서 이 구간을 나타내는 추상 타입 I를 추가합니다.
이 시점에서 Univalence 공리는 정리로 도출될 수 있습니다.
물론 계산됩니다.
몇 가지 원시 함수가 있습니다.
모두 다루지는 않겠습니다.
실제로 Cubical 타입에서 제거하는 방법을 제공할 수 있습니다.
이러한 추가 생성자로 패턴 매칭을 하는 우리 세계에서 일종의 결과가 나옵니다.
그게 Cubical 타입 이론이었고, 이제 Cubical Agda 자체는 이러한 종류의 기능과 함께 풀링 및 각 HIT에 대한 패턴 매칭의 더 깊은 통합을 갖춘 Agda 증명 보조 도구의 확장입니다.
Agda의 패턴 매칭에서 유도 타입을 처리합니다.
구간이 실제로 이론의 타입이라는 것과 같은 몇 가지 기술적인 사항과 제한 타입 등이 있습니다.
GitHub에 라이브러리가 있습니다.
여기에서 예제 및 필요한 것들의 코드베이스를 늘리고 있습니다.
이것을 사용하는 사람이 주요 개발자뿐만이 아니라는 것을 아는 것이 좋습니다.
GitHub에 추가하면 나타나는 기여자가 있습니다.
자세히 살펴보겠습니다.
두 끝점이 i0과 i1로 쓰여진 이 구간 타입 I가 있습니다.
이것들은 생성자처럼 보이지만 실제로는 이것들에 대해 패턴 매칭을 할 수 없습니다.
그리고 ex 변수의 타입군에서 경로 개념이 있습니다.
따라서 이 경로 P 타입 형성자가 있습니다.
이것은 새로운 원시 타입 형성자이며, 타입군과 구간의 0 쪽에 있는 것, 타입군의 1 쪽에 있는 것을 취합니다.
이것들은 실제로 일종의 오버로드이며, 시스템에서 특수한 종류의 함수로 취급됩니다.
구간에서 간단한 함수가 있으면 항상 이러한 경로 중 하나를 제거하여 만들 수 있습니다.
이러한 경로 중 하나가 있으면 요소 i에 적용하여 i에서 a를 얻을 수 있습니다.
우리가 얻는 것은 이것들이 0과 1에서 끝점을 추적한다는 것입니다.
예를 들어, a0과 a1 사이의 해당 타입의 경로 p가 있으면 0과 1에 적용할 때 무엇을 할지 이미 알고 있습니다.
따라서 이러한 추가 감소 규칙이 있습니다.
그런 다음 이 설정에서 일반적인 귀납적으로 정의된 동질성 대신 이 경로 타입의 동종 버전을 표준 동질성으로 사용할 수 있습니다.
Agda에서 특정 예를 살펴보겠습니다.
스트림을 정의하는 한 가지 방법은 두 개의 투영을 갖는 레코드로 정의하는 것입니다.
하나는 스트림의 헤드를 제공하고 다른 하나는 나머지, 즉 꼬리를 제공합니다.
그리고 이것이 귀납적 타입이 될 것이라고 선언하기만 하면 됩니다.
이것은 주로 종료 추적 또는 생산성을 처리합니다.
그런 다음 각 코드 패턴에 대해 수행하는 작업을 말하여 함수를 정의할 수 있습니다.
map을 정의하려면 이 map 항과 요소의 헤드를 투영할 때 발생하는 일과 꼬리를 투영할 때 발생하는 일을 말하면 됩니다.
이것은 스트림 사이의 경로를 정의하는 것으로 자연스럽게 확장됩니다.
이 예에서와 같이 스트림 사이의 경로입니다.
map s id x는 스트림을 정의해야 하므로 구간 인수인 추가 i 인수가 있습니다.
그리고 이 시점에서 세 번째 인수에서 받은 후 스트림 자체를 생성해야 합니다.
그런 다음 코패턴을 사용하여 해당 트리를 정의할 수 있습니다.
예를 들어 여기에서 이 동질성 증명에서 공동 귀납 원리를 사용합니다.
스트림이 귀납적이라는 사실에서 비롯됩니다.
증명을 정의하고 있지만 자체적으로 정의하고 있지만 스트림에서 이러한 함수를 정의하고 있기 때문에 여전히 생산적입니다.
실제로 이야기하고 있는 두 스트림을 연결하는 것과 같은지 확인하기 위해 왼쪽을 1 또는 0으로 바꾸면 타입에서 얻는 해당하는 올바른 결과가 나오는지 확인할 수 있지만 시간 관계상 건너뛰겠습니다.
마지막으로 전체 증명을 거쳐 내부적으로 유사성에 의한 동질성을 정의하고 스트림의 동질성과 같음을 증명할 수 있습니다.
Homotopy 타입 이론에서 고차 유도 타입의 또 다른 응용 프로그램은 공간에 대해 호모토피까지 합성 방식으로 추론하는 것입니다.
공간을 해당 공간의 점과 경로가 무엇인지 제공하고 일부 타입에 경로 생성자로 제공하는 것으로 표현할 수 있습니다.
따라서 정사각형에서 시작하여 이런 식으로 감싸서 토러스를 정의할 수 있습니다.
그런 다음 기본 연산과 경로 생성자에 대한 패턴 매칭으로 함수를 정의할 수 있습니다.
예를 들어 여기에서 원도 정의했고 토러스와 두 원 사이를 오가는 맵이 있음을 증명했습니다.
원 쌍에 대해 패턴 매칭을 할 때 루프 생성자에 대한 경우도 제공해야 합니다.
루프 생성자는 본질적으로 구간에서의 함수이기 때문에 추가 구간 변수를 범위에 가져옵니다.
그리고 여기에서, 일반적으로 Homotopy 타입 이론에서 이 두 함수가 동치를 형성한다는 것을 증명하는 것은 매우 지루할 수 있습니다.
하지만 모든 것이 계산되기 때문에 패턴 매칭을 하고 각 경우를 처리하면 이들은 사소하게 서로의 역입니다.
그 자세한 내용을 살펴보는 대신 결론을 내리겠습니다.
Cubical Agda는 이제 Agda 2.6.0.1의 최신 릴리스에 포함되어 있으며 GitHub에서 확인할 수 있는 라이브러리가 있습니다.
많은 예제가 있습니다.
감사합니다.
온라인에서 질문이 있습니다.
구간 타입을 다른 타입처럼 취급한다고 말씀하셨는데, 그것에 대해 자세히 설명해 주시겠습니까? 무슨 뜻입니까? 왜 괜찮습니까? 네, 음, 일반적으로는 괜찮지 않습니다.
왜냐하면 Cubical 타입 이론의 타입은 구간 타입에 반드시 사용할 수 있는 것은 아닌 hcomp와 같은 연산을 가질 것으로 예상되기 때문입니다.
하지만 구간을 이러한 연산이 존재한다고 가정하지 않는 특수 유니버스에 넣을 수 있습니다.
Cubical 타입 작업을 위한 몇 가지 원시 함수를 제공했습니다.
이러한 원시 함수가 완전한 Cubical 타입 이론이라는 의미가 있습니까? 그 질문을 공식화하는 방법을 잘 모르겠습니다.
예를 들어 경로 타입이 동등함을 증명할 만큼 충분히 강력합니다.
Cubical 동질성 타입에 대한 것입니다.
그리고 또한 문제의 타입 형성자의 보편적 속성을 증명하기 위해 필요합니다.
Agda에서 HIT를 수행하는 사람들의 커뮤니티가 Cubical Agda로 이동하거나 이미 이동했다고 생각하십니까? 그렇다면 또는 그렇지 않다면 그 이유는 무엇입니까? 그들 중 일부는 그렇습니다.
또는 적어도 Cubical Agda를 시도해 보았습니다.
아직 한 가지 걸림돌은 동질성 증명에 대한 패턴 매칭이 곧 지원될 예정이라는 것입니다.
따라서 전환이 용이해질 것입니다.
Agda는 최고의 대화형 환경으로 유명합니다.
Cubical 타입 이론이 사용자를 위해 대화형으로 사물을 구축하는 데 새로운 과제를 제기하는지 궁금했습니다.
그렇다면 어떻게 해결했습니까? 한 가지는 Cubical Agda에서 항상 열린 목표에 대한 동질성 제약 조건을 수집할 수 있지만 Cubical Agda에서는 경로에 대한 람다를 도입할 때마다 그렇게 됩니다.
따라서 최근 릴리스 또는 마스터에서 목표를 인쇄할 때 제약 조건을 인쇄하기 시작했으며, 이는 도움이 됩니다.
큐브 범주의 관점에서 Cubical Agda가 구현하는 Cubical 타입 이론의 종류는 무엇입니까? 드모르간 큐브, 네.
setoid 기반 증명을 모두 Cubical Agda를 사용하여 다시 작성해야 합니까? 그렇게 생각합니다.
지원하는 고차 유도 타입의 종류에 대해 조금 더 자세히 설명해 주시겠습니까? 현재 엄격한 양성을 통과하는 모든 것입니다.
경로의 끝점에 추가 조건을 두지 않습니다.
정규화를 깨뜨리는 것이 있을 것 같습니다.
그리고 기꺼이 예를 들어보겠습니다.
엄격한 검사를 하는 것입니다.
실제로 귀납적 타입에 대한 동질성 추론을 할 수 있다는 것을 알게 되어 기쁩니다.
하지만 Agda에서는 스트림보다 복잡한 귀납적 타입에 대한 크기 타입도 있습니다.
크기 타입과 Cubical 타입 사이에 특별한 상호 작용이 있습니까? 아니면 그냥 바로 작동합니까? 엄밀히 말하면 바로 작동하지만 좋은 결과를 얻지는 못합니다.
문제는 크기 타입이 제대로 작동하려면 언어에 일종의 크기 무관 원칙이 필요하지만 현재 크기는 다른 함수 인수와 같기 때문에 그러한 무관성을 알 수 없으므로 일반적인 보편적 속성을 증명할 수 없습니다.
여기서는 경로조차도 원하지 않을 것입니다.
좋아요.