ПС
{-# language Strict #-}Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 24
K
[
и что? Типы всё равно сойдутся
АП
AC
А что такое, по-вашему, "теории"?
АП
коротко говоря, множество формул(высказываний?)😊
соответствие Карри-Говарда это о том что одно высказывание в логике соответствует одному типу в ЯП.
Можно ли сформулировать (существует ли) соответствие, в котором одна теория в логике соответствует одному типу в ЯП?
соответствие Карри-Говарда это о том что одно высказывание в логике соответствует одному типу в ЯП.
Можно ли сформулировать (существует ли) соответствие, в котором одна теория в логике соответствует одному типу в ЯП?
АП
то есть получается что теория населена формулами, а тип населён термами.
правда, я не могу чётко сформулировать различие между формулами и термами🤔🧐
правда, я не могу чётко сформулировать различие между формулами и термами🤔🧐
AC
А в чём проблема завести тип "все высказывания в некоторой теории"? При наличии формализации указанной теории в имеющейся теории типов (в случае, когда это возможно).
AC
Нет принципиального различия между формулами и термами — тут мы просто про разные теории говорим. Поэтому термы одной теории соответствуют доказательствам в другой. Мы так это построили.
АП
Объявляю вас дефрагментатором моего мозга☺️
AC
Считаете, что у Вас есть мозг, и поэтому Вы — лучше нас?! 😂
h
По дефрагментации это вы не по адресу)
🐼
🐼
АП
А кто сказал что у вас нет мозга?
АП
про фрагментацию я не писал)
АП
Значит у вас вместо мозга что то другое, не менее мощное. Или вы не человек😁
NR
Надеюсь не исключающее
AG
скорее наоборот, не чихают ;)