Что составляет действительный тип бережливого производства?

Я прочитал первые 3 главы руководства по бережливому производству и уже сделал несколько доказательств в логике высказываний.

Теперь я пытаюсь немного вернуться назад и задавать себе глупые вопросы.

Я так понимаю:

  1. Термины могут иметь типы: constant A : Type. A - это термин, Type - это тип A.
  2. Термины могут стать типами: constant a : A.
  3. Тип термина может зависеть от типа другого термина: constant B : A -> Type, который является сахаром для constant B' : Π (a : A), Type

Но это понимание явно неверно, поскольку в этом коде не выполняется проверка типов:

constant A : Type

constant a : A

constant B : A -> Type

constant B' : Π (a : A), Type

constant C : Π (b : B), Type

constant C' : Π (B : A), (Π (b : B), Type)

constant C'' : B -> Type

Все строки, начинающиеся с constant C, то есть строки 9, 11 и 13, вызывают ошибку error: type expected at B

Почему? Я подозреваю, что не все термины могут стать типами. Я подозреваю, что термины, типы которых зависят от других типов, не могут стать типами. Почему?


theorem-proving proof lean
person Adam Kurkiewicz    schedule 07.12.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Ошибка первого типа

Проблема с ошибкой первого типа в

constant C : Π (b : B), Type

заключается в том, что вы не можете сказать b : B, потому что B - это функция (без определения) типа A -> Type, то есть B - это значение, а не тип. Нет смысла делать претензии типа b : 1, b : "xyz" или b : (λ a : A, Type).

Например. следующее будет работать, поскольку B a : Type:

constant C : Π (b : B a), Type

Ошибка второго типа

Ошибка второго типа в

constant C' : Π (B : A), (Π (b : B), Type)

проистекает из того факта, что неизвестно, является ли B типом, все, что мы знаем о B, это то, что это некое значение (житель) типа A. Чтобы использовать B таким образом, вам понадобится что-то вроде этого:

constant C' : Π (B : Type), (Π (b : B), Type)

т.е. мы явно говорим, что B - это тип.

Ошибка третьего типа

constant C'' : B -> Type

Причина, по которой не удается выполнить проверку типов, та же, что и в первом случае. B - это значение функции, а нам здесь нужен тип - поэтому constant B : A -> Type работает.

person Anton Trunov    schedule 08.12.2016
comment
Большое спасибо, это действительно помогает прояснить мое понимание. В частности, я убежден, что B - это функция, для обеих этих строк typecheck: check (B : (Π (a : A), Type)) и check ((λ (a : A), A) : (Π (a : A), Type)). Я убежден, что B имеет тот же тип, что и (λ (a : A), A), и поэтому я убежден, что B - это функция. Это очень интересно, и я этого не осознавал. - person Adam Kurkiewicz; 08.12.2016
comment
(1) Да, но я считаю, что вы имели в виду Type вместо Prop (или вам нужно изменить определения A и B) (2) constant - это способ постулировать некоторые вещи, не давая им реального определения. constant следует использовать с осторожностью, потому что это может внести несоответствия в вашу разработку - вы не захотите случайно ввести что-то эквивалентное constant f : false (или axiom f : false). - person Anton Trunov; 08.12.2016
comment
Вернемся к ошибке первого типа. B - это значение (типа A -> Type), но не тип. Однако A одновременно является значением и типом. Чтобы увидеть, что это значение, обратите внимание на constant A : Type. Чтобы увидеть, что это тип, обратите внимание на constant a : A. Я вижу, что значения, которые являются функциями, не могут становиться типами. Могут ли все другие значения (т.е. значения, которые не выполнять функции) стать типами? Если использовать чисто синтаксический подход, почему бы b : (λ a : A, Type) не иметь смысла? (Я понимаю, что семантически это полная чушь). - person Adam Kurkiewicz; 08.12.2016
comment
(1) Спасибо, я изменил Prop на Type в своем комментарии. - person Adam Kurkiewicz; 08.12.2016
comment
(2) Спасибо, я это понимаю. До того, как я узнал о sorry, я использовал свою собственную штуку, которая позволяла мне временно доказывать любое предположение axiom always : Π (p : Prop), p. Очевидно, я бы прокомментировал это после завершения доказательства: github.com/picrin /lean/blob/master/deMorgan.lean#L11 - person Adam Kurkiewicz; 08.12.2016
comment
Синтаксически (λ a : A, Type) не является типом, потому что он начинается с λ (или fun). - person Anton Trunov; 08.12.2016
comment
Я понимаю. Таким образом, можно сделать вывод, что каждый термин может стать типом, если только его тип не является функцией. - person Adam Kurkiewicz; 08.12.2016
comment
Извините, возможно, это слишком надумано. консервативный вывод: термины, являющиеся функциями, не могут становиться типами. Мой предыдущий вывод немного более авантюрный (но, возможно, тоже верный). - person Adam Kurkiewicz; 08.12.2016
comment
Все, что не живет в Type, не является типом. Не в моей голове: уже упомянутые функции (λ / fun), конструкторы данных (zero, succ и т. Д.), Конструкторы типов (list, vector). - person Anton Trunov; 08.12.2016
comment
В случае сомнений вы можете использовать check (<something> : Type), чтобы убедиться, что вы понимаете природу <something>. - person Anton Trunov; 08.12.2016