xavierm02

general recent conversations

$Mathematics$ Discussion between xavierm02 and kram…

Imported from a comment discussion on math.stackexchange.com/q...

xavierm02

Aug 25, 2017 15:13

I'll can try to write an answer summarizing what has been said in chat, but not right now.

xavierm02

Aug 25, 2017 15:08

Also, if you write $B^A = B x B x ... x B$, it feels weird to differentiat with respect to A.

xavierm02

Aug 25, 2017 15:07

In conclusion, I don't think zippers are relevant for functions ^.^

xavierm02

Aug 25, 2017 15:02

Well that works when the domain is finite.

xavierm02

Aug 25, 2017 15:02

All I'm saying is that a function can be seen as a big product type / record.

xavierm02

Aug 25, 2017 15:00

and then f is represented as c(f(1),f(2),f(3))

xavierm02

Aug 25, 2017 14:59

one constructor c of arity |{1,2,3}|=3

xavierm02

Aug 25, 2017 14:54

And when looking at it this way, modifying an element of type A doesn't really make sense.

xavierm02

Aug 25, 2017 14:53

Another argument to say that the zipper shouldn't touch elements of type A. You can think of elements of an inductive types as labeled trees, where nodes are labeled by constructor and have as subtrees the arguments given to those constructors. Similarly, f:A->B can be though of a tree of depth one where there is a single constructor of arity |A| at the root. So while for inductive types the zipper does have to move, for functions, since the depth is only one it doesn't have to move.

xavierm02

Aug 25, 2017 14:26

Well... I guess it depends what you call a set. But I'd expect enumerating elements to be part of the interface.

xavierm02

Aug 25, 2017 14:24

I means "
If A is not recursively enumerable, **an element of** A->bool isn't really a set because you can't enumerate its elements."

xavierm02

Aug 25, 2017 14:22

an element of A->bool*

xavierm02

Aug 25, 2017 14:22

If A is not recursively enumerable, A->bool isn't really a set because you can't enumerate its elements.

xavierm02

Aug 25, 2017 14:21

It's more like, since A may not be recursively enumerable, unless you are given a key, you can't do anything with a A->bool.

xavierm02

Aug 25, 2017 14:20

Not represented as A->bool, no.

xavierm02

Aug 25, 2017 14:15

Exactly. In a way, a function A->B doesn't contain elements of A, it only uses them. It does "contain" elements on B though.

xavierm02

Aug 25, 2017 14:08

Or more precisely $\partial_X B(X)^A=\partial_X B(X) \times B(X)^{A-1}$.

xavierm02

Aug 25, 2017 14:07

Btw, it should be $\partial B^A=\partial B \times B^{A-1}$:

xavierm02

Aug 25, 2017 14:06

there is no mathjax in chat -.-

xavierm02

Aug 25, 2017 14:05

crap

xavierm02

Aug 25, 2017 14:05

But if you think of $\partial_A X$ as "the zipper-like structure on $X$ that edits $A$s", then $\partial_B B^A$ makes sense because you change the values of the function but $\partial_A B^A$ doesn't because you shouldn't change values of type $A$ in a function: you take all of them.

xavierm02

Aug 25, 2017 14:05

If you see a zipper as some way of moving around and modifying the structure in a functional way, then for functions, you don't need to move around and $\operatorname{change_value}(f, k, v):=\lambda x. \operatorname{if} x = k \operatorname{then} v \operatorname{else} f(x)$ allows you to change the value. So if by $\partial_A B^A$ you mean "the zipper-like structure on $B^A$", it makes sense to set $\partial_A B^A \equiv B^A$.

xavierm02

Aug 25, 2017 14:05

It does kind of make sense to have $\partial_B B^A=B \times B^{A-1}$: you represent $f:A\to B$ as $(f(x),f_{|A\setminus\{x\}})$ for some $x\in A$. So maybe it's more that you can't differentiate with respect to types that are in a contravariant position.

xavierm02

Aug 25, 2017 14:05

The problem is that I don't see a good way of interpreting minus. For division, in the presentation of bags at the end of this paper, they quotient by automorphisms instead of dividing by the factorial. You could also try to use the series expansion of the logarithm. But really, if you want to extend the zipper to functions, you probably should just set $\partial_A B^A\cong B^A$ because the whole point of the zipper is to move around to edit the structure in a functional way, and this can be done directly for functions.

xavierm02

Aug 25, 2017 14:05

In the papers you link to, derivation seems to only be defined for positive types but $A\to B$ is a negative type. Do you know a specific paper defining the derivative on function types? I'd expect things to still kind of work for coinductive types but it looks really weird for function types. The zipper uses the tree-like structure of the term and a function has no such structure.

$Mathematics$ Discussion between xavierm02 and Hask…

Imported from a comment discussion on math.stackexchange.com/q...

xavierm02

Feb 16, 2017 14:55

@HaskellFun Both are the same I think. If you look at "a->b" as "not(a) \/ b", and since we don't consider models with empty domains, you can get the ∃ outside of the arrow. Then you can swap if with the first order ∃ and you've got your first formula.

xavierm02

Feb 16, 2017 14:39

I'm not sure yet how to remove the second order forall quantifiers though.

xavierm02

Feb 16, 2017 14:38

Ok. I think I have a good argument to say that you can't characterise finiteness in MSO over the empty signature.
First, replace all "x = y" by "forall P, P x <-> P y".
Then, do the transformation to put all second order quantifiers first, then all first order quantifiers and finally the boolean stuff. It's also second order quantifier followed by a monadic first order formula. And monadic first order formulas have the finite model property (because you can say that two elements of the model are equivalent if they are in the same predicates, and then the quotient model is still a model and …

xavierm02

Feb 15, 2017 17:13

if it's some exists and some forall, you have to use a trick

xavierm02

Feb 15, 2017 17:12

if poth are the same it's trivial

xavierm02

Feb 15, 2017 17:12

What is says, basically, is that you can always push the second order quantifiers before the first order ones

xavierm02

Feb 15, 2017 17:12

You can use the transformation on page 16 here though: logic.at/lvas/185301/Leivant_higher-order-logic.pdf

xavierm02

Feb 15, 2017 17:11

I need to go now, I'll come back later to recheck.

xavierm02

Feb 15, 2017 17:11

But it looks like it's fine.

xavierm02

Feb 15, 2017 17:10

You don't need z' to be in X and Y. It's implied by being in closure(Z).

xavierm02

Feb 15, 2017 17:02

I thought you were talking about the formula for path

xavierm02

Feb 15, 2017 17:02

aaaaah

xavierm02

Feb 15, 2017 16:49

Both.

xavierm02

Feb 15, 2017 16:28

Wait. The formula is of the form <-- second order quantifiers --> <-- first order quantifiers --> <-- boolean stuff -->

xavierm02

Feb 15, 2017 16:26

I was looking at this to try to get ideas for the definability of finiteness but it could help you too: math.stackexchange.com/questions/2099964/…

xavierm02

Feb 15, 2017 16:25

You want the second order quantifiers on the outside

xavierm02

Feb 15, 2017 16:25

xavierm02

Feb 15, 2017 16:25

@HaskellFun I don't understand your question

xavierm02

Feb 15, 2017 15:04

or maybe not

xavierm02

Feb 15, 2017 15:04

First fix attempt: It should be, for all mu, M, mu |= F iff M, mu |= G

xavierm02

Feb 15, 2017 14:41

@user21820 Yeah. It's not a real argument, just some random thought.

xavierm02

Feb 15, 2017 13:25

@user21820 Well the only thing that changes is that you have a second type of forall quantifier. But it's still implicitly universally quantified so the induction step from F to forall P, F should work just as well. And then, there's a new base case P x. But since P is implicitly universally quantified, it means forall P, P x, which is false since for P the always false predicate, it's false. So you can take "at least 1 element and at most 0 element" or some other absurd statement.

xavierm02

Feb 15, 2017 12:50

(I'm really not sure but I couldn't find any reference so I tried to do it myself)

xavierm02

Feb 15, 2017 12:49

For forall x, F, you just take G (which should work because formulas are implicitly universally quantified). And for exists x, F, you take the G for not(forall x, (not (F))).

xavierm02

Feb 15, 2017 12:48

@user21820 Nope. I'd guess it's proved by induction on the formula. The exact property should be that for every formula F there are some "there are at least n elements" property whose boolean combination G is so that M |= F iff M |= G. It works for x=x because you can take "at least 0 elements" and for x=y because you can take "at most one element". Then, for boolean combinations of Fs, you take the same combinations of Gs.