相关疑难解决方法(0)

我在编程生涯中相对较晚地遇到了Curry-Howard Isomorphism,也许这有助于我对它完全着迷.这意味着对于每个编程概念,在形式逻辑中存在精确的模拟,反之亦然.这是一个关于这种类比的"基本"列表,在我的头脑中:

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

那么,对于我的问题:这种同构的一些更有趣/模糊的含义是什么？我不是逻辑学家,所以我确信我只是在这个清单上划过界限.

例如,这里有一些编程概念,我不知道逻辑中精辟的名字:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known …

我试图在Agda中证明一个简单的引理,我认为这是真的.

如果一个向量有两个以上的元素,那么采取head以下方法就init可以head立即采用它.

我的表述如下:

lem-headInit : ?{l} (xs : Vec ? (suc (suc l)))
                    -> head (init xs) ? head xs
lem-headInit (x ? xs) = ?

哪个给了我;

.l : ?
x  : ?
xs : Vec ? (suc .l)
------------------------------
Goal: head (init (x ? xs) | (initLast (x ? xs) | initLast xs)) ? x

作为回应.

我不完全了解如何阅读该(init (x ? xs) | (initLast (x ? xs) | initLast xs))组件.我想我的问题是; 是否有可能,该术语的含义和含义是什么.

非常感谢.