6 ms·
∆⊢e:A Can someone explain this (from p. 3) to me, or point me to an explanation? I am especially unsure about the usage of ∆ and : in this context.
by jraedisch 10y ago
∆⊢e:A
Can someone explain this (from p. 3) to me, or point me to an explanation? I am especially unsure about the usage of ∆ and : in this context.
- deleted 10y ago[deleted]
- mafribe 10y agoAs this paper is about a Curry-Howard correspondence, the statement has two (equivalent) readings. Reading 1. It's a typing judgement. You can read ∆⊢e:A as "the program e has type A, assuming the free variables in e are typed as described by ∆". Reading 2. It's a logical judgement. You can read ∆⊢e:A as "the proof e is a proof of the logical formula A, assuming the free variables in the proof e stand in for proofs as described by ∆".
- jraedisch 10y agoThanks! I took a look at the Wiki page https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... but didn't see any Deltas there.
- mafribe 10y agoLogical and typing judgements can be presented in many different ways, triples like ∆⊢e:A being one of them.
- s_ngularity 10y agoA great overview of this stuff is http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
- jraedisch 10y agoAnd this one actually has Deltas in it. Thanks!
- greydius 10y agoIt's common to use Γ (gamma) as well.