Andreas Stuhlmüller stuhlmueller

User: Can you explain proof nets and the geometry of interaction to me in crisp, clear terms?

Assistant: Sure, I'll do my best to explain these concepts in a simple way.

Proof Nets: Proof nets are a graphical representation of proofs in linear logic. They were introduced to overcome the problem of redundancy in the sequent calculus representation of proofs. In simple terms, proof nets are a way to represent logical proofs as graphs, where nodes represent logical operations and edges represent the flow of information. They provide a way to check the correctness of a proof in a more efficient manner than traditional methods.
Geometry of Interaction (GoI): The Geometry of Interaction is a mathematical framework that was introduced to understand the dynamics of computation in linear logic and other computational systems. It provides a geometric interpretation of computation, where computations are seen as movements in a geometric space.

Elicit tasks as fold and unfold

Many of the tasks we care about either expand a tree by one layer (add factors, subquestions, datasets) or summarize a tree layer into one or a few nodes (summarize, cluster, rank).

This raises two questions:

Is there an existing way to characterize these tasks so that we can make an app that supports all and only the ones we want?
Language models have a finite context window. How can we clearly think about tasks that operate on arbitrarily large inputs?

Technically, we can think of expansion tasks as unfolds (creating structure) and summarization-like tasks as folds (reducing structure). They're defined like this:

Keybase proof

I hereby claim:

I am stuhlmueller on github.
I am stuhlmueller (https://keybase.io/stuhlmueller) on keybase.
I have a public key whose fingerprint is E5E1 83AF 5944 BC22 E0D9 65E9 3E9E EE48 AE46 5D41

To claim this, I am signing this object:

	"""
	Converts a directory with Rev.com transcripts into the dataset format required by Elicit.

	Format for transcripts:

	https://www.rev.com/transcript-editor/Edit?token=12312

	Jane Doe:
	Good morning. Thank you everyone for joining our webinar. My name is Jon Doe.

	var model = function() {
	var x = uniform(0,1);
	var yERP = Enumerate(function(){
	return flip(x);
	})
	var y = sample(yERP);
	return x + y;
	}

	MCMC(model, { kernel: { HMC: { steps: 10, stepSize: 1 }},

	function MCMC(s, k, a, wpplFn, options) {

	var options = _.defaults(
	_.clone(options),
	{ samples: 100,
	kernel: MHKernel,
	lag: 0,
	burn: 0 });

	var log = function(s) {

	(defun codex-refactor (&optional b e)
	(interactive "r")
	(shell-command-on-region b e "codex-refactor.py" nil nil))

	(defun codex (&optional b e)
	(interactive "r")
	(shell-command-on-region b e "codex.py" nil nil))