Newest at the top
| 2026-02-07 13:06:59 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-02-07 13:06:07 +0100 | jreicher | (~joelr@user/jreicher) (Remote host closed the connection) |
| 2026-02-07 13:06:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-07 13:05:22 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-02-07 13:00:30 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-02-07 12:58:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:55:07 +0100 | <ski> | (i was recently starting to formulate (optimized) CPS-transformation, first in lambdaProlog (which also has matching on HOAS, but not dependent types), then trying to do it in Twelf, for comparision .. ran out of steam, after a while, fighting with it to accept some parts, though) |
| 2026-02-07 12:53:45 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-02-07 12:50:53 +0100 | <ski> | .. i can't keep from feeling like there ought to be a way to address those concerns more directly .. rather than resorting to going to a different (functional) computational model. Twelf is the only dependently typed logic programming language i'm aware of, and it would seem to be a shame to not further develop that |
| 2026-02-07 12:50:36 +0100 | Beowulf | (florian@2a01:4f9:3b:2d56::2) |
| 2026-02-07 12:49:25 +0100 | <ski> | the issue being limitations in reasoning about local parameters (data constructors), and local assumptions, for the mode-checking. and, perhaps, also some limitations in doing (effectively) anonymous predicates, e.g. extending an accumulator predicate parameter -- and associated reasoning about mode for such higher-order predicates |
| 2026-02-07 12:47:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 12:47:13 +0100 | <ski> | said above (meta-)proof checking) |
| 2026-02-07 12:47:06 +0100 | <ski> | one of the reasons they stated for developing Delphin (rather than Twelf), was a claim of having trouble with some kinda of higher-order programming. afaict, what they mean by this is not lack of support for higher-order predicates, per se, but rather lack of adequate support for the static mode&determinism *checking* (which is optional (from a computational standpoint), but essential for when you want to do |
| 2026-02-07 12:46:32 +0100 | Beowulf | (florian@2a01:4f9:3b:2d56::2) (Quit: = "") |
| 2026-02-07 12:44:18 +0100 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-02-07 12:42:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:35:26 +0100 | <ski> | it also has facilities to be able to state such theorems, and let a theorem-prover (in the language implementation) search for a proof (and realize it as a recursive predicate) |
| 2026-02-07 12:34:27 +0100 | <ski> | so, the system has facilities to do this (meta-proof) checking of modes, in order to ensure that the predicate whose definition encodes your proof actually proves the intended thing (e.g. that if an (object-language) term has some type, and you reduce the term one step, then it still has that type) |
| 2026-02-07 12:33:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-07 12:32:43 +0100 | <ski> | mode&determinism declaration on the predicate (if you will, ensuring that the relation is functional) |
| 2026-02-07 12:32:37 +0100 | <ski> | one of the interesting things you can do in Twelf, is to encode a proof as a relation. to actually check that the proof is valid, you then need to check that for each possible input for some designated input parameters to the relation/predicate, there is a related output asssigned to the output parameter(s), such that the (dependently typed) relation holds. from a logic programming standpoint, this is a |
| 2026-02-07 12:28:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:24:11 +0100 | _JusSx_ | (~jussx@78.211.193.248) |
| 2026-02-07 12:23:30 +0100 | <ski> | schematic variables to fill in with other LF terms) |
| 2026-02-07 12:23:24 +0100 | <ski> | (ooc, they also had effectively a monad, in the language, for computations which will result in a value term of an LF type. the type `<T>' is short for `T * unit', which is short for `exists _ : T. unit'. in `T * U', `U' is not allowed to be an LF type, but `T' is. the reason is that they want all expressions of LF type to not have any computational (Delphin-level) subexpressions, only an LF-term, with some |
| 2026-02-07 12:22:25 +0100 | _JusSx_ | (~jussx@78.210.148.66) (Ping timeout: 245 seconds) |
| 2026-02-07 12:19:36 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-02-07 12:19:19 +0100 | <ski> | in the case of the functional programming (Delphin), they choose to instead allow you to add patterns for "parameters" of (LF) types, in your `case'-`of' expressions (and then you'd often also pass some kind of accumulating substitution function, or similar, to the traversal function, initializing it to the empty function at the top call) |
| 2026-02-07 12:17:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-07 12:17:32 +0100 | <ski> | in the case of logic programming (Twelf), you'll be dynamically (similar to dynamic scope, being the operational interpretation of implicational logic programming goals here) adding clauses to your recursive traversal predicates, as you step under the binders |
| 2026-02-07 12:16:07 +0100 | <ski> | so, `x',`f',`f',`x' (four different variables, the language automatically ensures no clashes, capture-free substitution) here will, in the local contexts, act as new temporary data constructors for the expression data type (with `app' and `lam' as the *only* global data constructors, in this example of pure lambda calculus) |
| 2026-02-07 12:13:30 +0100 | <ski> | if you match on and do recursion on an LF term like `app (lam x\ lam f\ f x) (lam f\ lam x\ f x x)' (representing `(\x. \f. f x) (\f. \x. f x x)', where `app : expr (A -> B) -> (expr A -> expr B)' and `lam : (expr A -> expr B) -> expr (A -> B)'), you'll need to step inside the binders, traversing open terms |
| 2026-02-07 12:12:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:09:26 +0100 | ski | was reading, recently, about a (rather restricted, in various ways) dependently typed functional language (Delphin, meant as a different approach to the logic programming approach Twelf to LF terms) for doing computation over LF (Logical Framework) terms, typically used to represent HOAS (that you can *pattern-match* on !) |
| 2026-02-07 12:04:22 +0100 | <ski> | (.. in some cases, one might be able to get away with generating something like `\[a,b,c,...,z] -> ...' for an indefinite number of elements in the list pattern, but still keep the simple static types) |
| 2026-02-07 12:03:13 +0100 | <ski> | provides) |
| 2026-02-07 12:03:07 +0100 | <ski> | (depending on what one'd want to do ?) i think one could possibly do that kind of thing, in MetaML or MetaOCaml, with their quasiquoted code expressions. one'd need to introduce local (quoted) binders for them, though. and, i guess, might need to either resort to dynamically typed code expressions (which at least MetaML provides, i forget about MetaOcaml), or else to dependent typing (which neither of them |
| 2026-02-07 12:02:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 11:58:53 +0100 | <ski> | .. presumable that F# binding can do that, as well ? |
| 2026-02-07 11:58:24 +0100 | <ski> | i suppose sometimes you'd like to generate fresh variables (perhaps in a loop, or in a recursive computation) .. |
| 2026-02-07 11:57:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:48:33 +0100 | <int-e> | jreicher: So basically, it's a different flavor of name clashes than variable capture. |
| 2026-02-07 11:46:35 +0100 | <int-e> | Oh also I think terms are first-order, so there are no binders that could capture variables. |
| 2026-02-07 11:46:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-02-07 11:45:22 +0100 | <int-e> | No, there's no substitution taking place. There's a global namespace. But users may want to generate auxiliary variables without clashing with other auxiliary variables, so as a convenience, fresh name generation is provided by the SMT solver. (At no real cost; the SMT solver will need that functionality internally anyway.) |
| 2026-02-07 11:42:51 +0100 | AlexZenon | (~alzenon@85.174.182.86) |
| 2026-02-07 11:42:27 +0100 | <jreicher> | int-e: I'm not familiar with Z3, but is the generation of fresh names a crappy implementation of capture-avoiding substitution? |
| 2026-02-07 11:42:00 +0100 | qqq | (~qqq@185.54.22.56) (Quit: Lost terminal) |
| 2026-02-07 11:41:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |