Где-то я слышал, что этимология примерно такова: - Π является типом для ∀-выражений. Предикат ∀a:A.Ba можно представить как коньюнкцию Ba0∧Ba1∧Ba2∧... ∧ можно сравнить с произведением (в каком контексте, сказать не могу. В булевом кольце and вроде как произведение, но там с коньюнкцией нестыковка. Можно представить and и or как операции над множествами, но я не знаю как эта модель называется). Ну так вот, ∧ соответствует произведению, поэтому Π-тип называют зависимым произведением (dependent product);
- Σ — вроде как, тип для ∃-выражений. Предикат ∃a:A.Ba можно представить как Ba0∨Ba1∨Ba2∨... ∨ является аналогом суммы, поэтому Σ-тип называют зависимой суммой (dependent sum).
Если элементов в A слишком много, то коньюнкции и дизьюнкции получаются бесконечными. Не конструктивно. Ходят легенды, что в стане интуиционистов Π и Σ-типы назывались иначе: - с конструктивной точки зрения, предикат ∀a:A.Ba говорит о том, что у нас есть способ построения объекта Ba для каждого объекта a∈A. Т.е. есть некоторая функция из A в Ba. А Πa:A.Ba — обобщение функционального типа. Поэтому его называют зависимым функциональным типом dependent function type;
- ∃a:A.Ba значит, что у нас есть пара: объект a∈A и объект Ba (который мы смогли построить из а). Поскольку пара является элементом произведения двух множеств, то Σ-тип называют зависимым произведением dependent product (ага, в первом варианте было совсем наоборот).
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2008-06-10 11:44 am (UTC)Где-то я слышал, что этимология примерно такова:
- Π является типом для ∀-выражений. Предикат ∀a:A.Ba можно представить как коньюнкцию Ba0∧Ba1∧Ba2∧...
∧ можно сравнить с произведением (в каком контексте, сказать не могу. В булевом кольце and вроде как произведение, но там с коньюнкцией нестыковка. Можно представить and и or как операции над множествами, но я не знаю как эта модель называется). Ну так вот, ∧ соответствует произведению, поэтому Π-тип называют зависимым произведением (dependent product);
- Σ — вроде как, тип для ∃-выражений. Предикат ∃a:A.Ba можно представить как Ba0∨Ba1∨Ba2∨...
∨ является аналогом суммы, поэтому Σ-тип называют зависимой суммой (dependent sum).
Если элементов в A слишком много, то коньюнкции и дизьюнкции получаются бесконечными. Не конструктивно.
Ходят легенды, что в стане интуиционистов Π и Σ-типы назывались иначе:
- с конструктивной точки зрения, предикат ∀a:A.Ba говорит о том, что у нас есть способ построения объекта Ba для каждого объекта a∈A. Т.е. есть некоторая функция из A в Ba. А Πa:A.Ba — обобщение функционального типа. Поэтому его называют зависимым функциональным типом dependent function type;
- ∃a:A.Ba значит, что у нас есть пара: объект a∈A и объект Ba (который мы смогли построить из а). Поскольку пара является элементом произведения двух множеств, то Σ-тип называют зависимым произведением dependent product (ага, в первом варианте было совсем наоборот).
Вроде, как-то так.