The Beginning of the Next Steps of Project Awesome.
Set up your quiz:
Enter a seed (in hexadecimal) for this quiz.
(If none is provided, one will be generated randomly.)
Seed:
Quiz Title:
Select how many questions of each type you'd like your quiz to have.
Click "Generate Quiz" to generate a new quiz according to the settings above.
Alternately, click "Load JSON" to load a quiz from a JSON file. (It will still use the seed specified above.)


--- layout: page title : Team Profiles group: navigation weight: 3 --- Meet The Team Jimmy NguyenLaw Clerk Nazi RejaliParalegal Omid RejaliAttorney Chris NepacenaLaw Clerk Vivek PoolaI.T. Support/Development Omid RejaliAttorney Chris NepacenaLaw Clerk Jimmy NguyenLaw Clerk Vivek PoolaI.T. Support/Development Nazi RejaliParalegal {% include themes/rejalilaw/location.html %} SOCIAL {% include themes/rejalilaw/social.html %}
Law Clerk
Paralegal
Attorney
I.T. Support/Development
SOCIAL
{% include themes/rejalilaw/social.html %}


BIBUTILS(1) User Commands BIBUTILS(1) NAME bibutils - bibliography conversion utilities SYNOPSIS format2xml [OPTIONS] [file.format] xml2format [OPTIONS] [file.xml] DESCRIPTION The bibutils program set inter-converts between various bibliography formats using Library of Congress[1]'s Metadata Object Description Schema (MODS)[2]version 3.1. For example, one can convert RIS-format files to Bibtex by doing two transformations: RIS->MODS->Bibtex. CONVERTING TO MODS Overview ll. Command Description T{ bib2xml T} T{ convert bibtex to MODS T} T{ biblatex2xml T} T{ convert biblatex to MODS T} T{ copac2xml T} T{ convert COPAC[3]format references to MODS T} T{ ebi2xml T} T{ convert EBI XML to MODS T} T{ end2xml T} T{ convert EndNote (Refer format) to MODS T} T{ endx2xml T} T{ convert EndNote XML to MODS T} T{ isi2xml T} T{ convert ISI web of science to MODS T} T{ med2xml T} T{ convert Pubmed XML references to MODS T} T{ modsclean T} T{ a MODS to MODS converter T} T{ ris2xml T} T{ convert RIS format to MODS T} T{ wordbib2xml T} T{ convert Word2007 bibliography XML to MODS T} Common Options Converting to MODS Several flags available for the end2xml, endx2xml, bib2xml, ris2xml, med2xml, and copac2xml programs. Most options have both a short and a long version. lll. T{ -h T} T{ --help T} T{ display help T} T{ -v T} T{ --version T} T{ display version T} T{ -a T} T{ --add-refcount T} T{ add "_#", where # is reference count to reference id T} T{ -s T} T{ --single-refperfile T} T{ put one reference per file name by the reference number T} T{ -i T} T{ --input-encoding T} T{ interpret the input file as using the requested character set (use w/o argument for current list derived from character sets at www.kostis.net[4]) unicode is now a character set option T} T{ -u T} T{ --unicode-characters T} T{ encode unicode characters directly in the file rather than as XML entities T} T{ -un T} T{ --unicode-no-bom T} T{ as -u, but don't include a byte order mark T} T{ -x T} T{ --xml-entities T} T{ encode unicode characters as XML entities (opposite of -u) T} T{ -nl T} T{ --no-latex T} T{ do not convert latex-style character combinations T} T{ -s T} T{ --single-refperfile T} T{ one reference per output file T} T{ -d T} T{ --drop-key T} T{ don't put citation key in the mods id field T} T{ -c T} T{ --corporation-file T} T{ with argument specifying a file containing a list of corporation names to be placed in <name type="corporate"></name> instead of type="personal" and eliminate name mangling T} T{ -a T} T{ --asis T} T{ with argument specifying a file containing a list of names be treated verbatim T} T{ -nt T} T{ --nosplit-title T} T{ don't split titles into TITLE/SUBTITLE pairs T} T{ T} T{ --verbose T} T{ verbose output T} T{ T} T{ --debug T} T{ very verbose output (mostly for debugging) T} bib2xml bib2xml converts a bibtex-formatted reference file to an XML-intermediate bibliography file. Specify file(s) to be converted on the command line. Files containing bibtex substitutions strings should be specified before the files where substitutions are specified (or in the same file before their use). If no files are specified, then bibtex information will be read from standard input. bib2xml bibtex_file.bib > output_file.xml biblatex2xml bib2xml converts a biblatex (not to be confused with bibtex) formatted reference file to an XML-intermediate bibliography file. . bib2xml biblatex_file.bib > output_file.xml copac2xml copac2xmlconverts a COPAC formatted reference file to a MODS XML-intermediate bibliography file. end2xml end2xml converts a text endnote-formatted reference file to an XML-intermediate bibliography file. This program will not work on the binary library; the file needs to be exported first. Endnote tagged formats ("Refer" format export) look like Example 1, “Example refer format file”. There are very nice instructions for making sure that you are properly exporting this at http://www.sonnysoftware.com/endnoteimport.html[5] Usage for end2xml is the same as bib2xml. end2xml endnote_file.end > output_file.xml ebi2xml ebi2xml converts a EBI XML file to a MODS XML-intermediate bibliography file. endx2xml endx2xml converts a EndNote-XML exported reference file to a MODS XML-intermediate bibliography file. This program will not work on the binary library; the file needs to be exported first. isi2xml isi2xml converts an ISI-web-of-science-formatted reference file to an XML-intermediate bibliography file. Usage for isi2xml is the same as bib2xml. isi2xml input_file.isi > output_file.xml ris2xml ris2xml converts a RIS-formatted reference file to an XML-intermediate bibliography file. ris2xml usage is as end2xml and bib2xml ris2xml ris_file.ris > output_file.xml wordbib2xml ris2xml converts a RIS-formatted reference file to an XML-intermediate bibliography file. ris2xml usage is as end2xml and bib2xml CONVERTING FROM MODS Overview ll. Command Description T{ xml2ads T} T{ convert MODS into the SAO/NASA ADS format T} T{ xml2bib T} T{ convert MODS into bibtex T} T{ xml2end T} T{ convert MODS into format for EndNote T} T{ xml2isi T} T{ convert MODS to ISI format T} T{ xml2ris T} T{ convert MODS into RIS format T} T{ xml2wordbib T} T{ convert MODS into Word 2007 bibliography format T} Common Options Converting from MODS Note that --output-encoding refers to the input file lll. T{ -h T} T{ --help T} T{ display help T} T{ -v T} T{ --version T} T{ display version T} T{ -o T} T{ --output-encoding T} T{ interpret the input file as using the requested character set (use w/o argument for current list derived from character sets at www.kostis.net[4]) unicode is now a character set option T} T{ -s T} T{ --single-refperfile T} T{ put one reference per file name by the reference number T} T{ -nb T} T{ --no-bom T} T{ do not write Byte Order Mark if writing UTF8 T} xml2bib xml2bib converts the MODS XML bibliography into a bibtex-formatted reference file. xml2bib usage is as for other tools xml2bib xml_file.xml > output_file.bib Since the BibTeX reference format is fairly flexible and seems to have the greatest number of personal preferences, it has also accumulated a number of specific options that are not available for other formats. Starting with 3.24, xml2bib output uses lowercase tags and mixed case reference types for better interaction with other software. The older behavior with all uppercase tags/reference types can still be generated using the command-line switch -U/--uppercase. xml2bib-specific Options: lll. T{ -fc T} T{ --finalcomma T} T{ add final comma in the bibtex output for those that want it T} T{ -sd T} T{ --singledash T} T{ use one dash instead of two (longer dash in latex) between numbers in page output T} T{ -b T} T{ --brackets T} T{ use brackets instead of quotation marks around field data T} T{ -w T} T{ --whitespace T} T{ add beautifying whitespace to output T} T{ -U T} T{ --uppercase T} T{ use all uppercase for tags (field names) and reference types (pre-3.24 behavior) T} T{ -sk T} T{ --strictkey T} T{ only use alphanumeric characters for bibtex citation keys T} xml2ads xml2ads converts the MODS XML bibliography to the Smithsonian Astrophysical Observatory (SAO)/National Aeronautics and Space Administration (NASA) Astrophyics Data System or ADS reference format[6] (which is very similar to the tagged Endnote style). xml2ads usage is as for other tools xml2ads xml_file.xml > output_file.ads xml2ris xml2ris converts the MODS XML bibliography to RIS-formatted bibliography file. xml2ris usage is as for other tools xml2ris xml_file.xml > output_file.ris xml2end xml2end converts the MODS XML bibliography to tagged Endnote (refer-format) bibliography file. xml2end usage is as for other tools xml2end xml_file.xml > output_file.end xml2wordbib xml2wordbib converts the MODS XML bibliography to Word 2007-formatted XML bibliography file. xml2wordbib usage is as for other tools xml2wordbib xml_file.xml > output_file.word.xml xml2wordbib was called xml2word in versions of bibutils prior to 3.40. It was renamed to avoid confusion with other tools. Hopefully this will not break too many scripts already in use. EXAMPLES Example 1. Example refer format file %0 Journal Article %A C. D. Putnam %A C. S. Pikaard %D 1992 %T Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers %J Mol Cell Biol %V 12 %P 4970-4980 %F Putnam1992 xml2bib Output Variations Example 2. Default @Article{Putnam1992, author="C. D. Putnam and C. S. Pikaard", year="1992", month="Nov", title="Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers", journal="Mol Cell Biol", volume="12", pages="4970--4980", number="11"} Example 3. Final Comma @Article{Putnam1992, author="C. D. Putnam and C. S. Pikaard", year="1992", month="Nov", title="Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers", journal="Mol Cell Biol", volume="12", pages="4970--4980", number="11",} Example 4. Single Dash @Article{Putnam1992, author="C. D. Putnam and C. S. Pikaard", year="1992", month="Nov", title="Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers", journal="Mol Cell Biol", volume="12", pages="4970-4980", number="11"} Example 5. Whitespace @Article{Putnam1992, author = "C. D. Putnam and C. S. Pikaard", year = "1992", month = "Jan", title = "Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers", journal = "Mol Cell Biol", volume = "12", pages = "4970--4980" } Example 6. Brackets @Article{Putnam1992, author={Putnam, C. D. and Pikaard, C. S.}, title={Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers}, journal={Mol Cell Biol}, year={1992}, month={Nov}, volume={12}, number={11}, pages={4970--4980} } Example 7. Uppercase @ARTICLE{Putnam1992, AUTHOR="Putnam, C. D. and Pikaard, C. S.", TITLE="Cooperative binding of the Xenopus RNA polymerase I transcription factor xUBF to repetitive ribosomal gene enhancers", JOURNAL="Mol Cell Biol", YEAR="1992", MONTH="Nov", VOLUME="12", NUMBER="11", PAGES="4970--4980" } LICENSE All versions of bibutils are relased under the GNU Public License (GPL). In a nutshell, feel free to download, run, and modify these programs as required. If you re-release these, you need to release the modified version of the source. (And I'd appreciate patches as well...if you care enough to make the change, then I'd like to see what you're adding or fixing.) Chris Putnam, Ludwig Institute for Cancer Research[7] COPYRIGHT Copyright © 2010 David Bremner (Manual) Copyright © 2008 Christopher Putnam (Software and Manual) This manual page is distributed under the terms of version 2 of the GNU General Public License. NOTES 1. Library of Congress http://www.loc.gov 2. Metadata Object Description Schema (MODS) http://www.loc.gov/standards/mods/ 3. COPAC http://copac.ac.uk/ 4. www.kostis.net http://www.kostis.net/ 5. http://www.sonnysoftware.com/endnoteimport.html http://www.sonnysoftware.com/endnoteimport.html 6. ADS reference format http://doc.adsabs.harvard.edu/abs_doc/help_pages/taggedformat.html 7. Chris Putnam, Ludwig Institute for Cancer Research http://www.scripps.edu/~cdputnam/ bibutils 4.12 December 10, 2010 BIBUTILS(1)


Package org.apache.qpid.protonj2.client
Class ConnectionOptions
- java.lang.Object
-
- org.apache.qpid.protonj2.client.ConnectionOptions
-
public class ConnectionOptions extends java.lang.Object
Options that control the behaviour of theConnection
created from them.
-
-
Field Summary
Fields Modifier and Type Field Description static int
DEFAULT_CHANNEL_MAX
static long
DEFAULT_CLOSE_TIMEOUT
static java.util.List<java.lang.String>
DEFAULT_DESIRED_CAPABILITIES
static long
DEFAULT_DRAIN_TIMEOUT
static long
DEFAULT_IDLE_TIMEOUT
static int
DEFAULT_MAX_FRAME_SIZE
static NextReceiverPolicy
DEFAULT_NEXT_RECEIVER_POLICY
static long
DEFAULT_OPEN_TIMEOUT
static long
DEFAULT_REQUEST_TIMEOUT
static long
DEFAULT_SEND_TIMEOUT
static long
INFINITE
-
Constructor Summary
Constructors Constructor Description ConnectionOptions()
Create a newConnectionOptions
instance configured with default configuration settings.ConnectionOptions(ConnectionOptions options)
Creates aConnectionOptions
instance that is a copy of the given instance.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description int
channelMax()
ConnectionOptions
channelMax(int channelMax)
Configure the channel maximum value for the newConnection
created with these options.ConnectionOptions
clone()
long
closeTimeout()
ConnectionOptions
closeTimeout(long closeTimeout)
Configures the timeout used when awaiting a response from the remote that a request to close a resource such as aConnection
,Session
,Sender
orReceiver
h as been honored.ConnectionOptions
closeTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a response from the remote that a request to close a resource such as aConnection
,Session
,Sender
orReceiver
h as been honored.java.util.function.BiConsumer<Connection,ConnectionEvent>
connectedHandler()
ConnectionOptions
connectedHandler(java.util.function.BiConsumer<Connection,ConnectionEvent> connectedHandler)
Configures a handler that will be notified when aConnection
has established.protected ConnectionOptions
copyInto(ConnectionOptions other)
Copy all options from thisConnectionOptions
instance into the instance provided.NextReceiverPolicy
defaultNextReceiverPolicy()
ConnectionOptions
defaultNextReceiverPolicy(NextReceiverPolicy policy)
Configures the default next receiver policy for this connection and any session that is created without specifying user defined session default options.java.lang.String[]
desiredCapabilities()
ConnectionOptions
desiredCapabilities(java.lang.String... desiredCapabilities)
Sets the collection of capabilities to request from the remote for a newConnection
created using theseConnectionOptions
.java.util.function.BiConsumer<Connection,DisconnectionEvent>
disconnectedHandler()
ConnectionOptions
disconnectedHandler(java.util.function.BiConsumer<Connection,DisconnectionEvent> disconnectedHandler)
Configures a handler that will be notified when the connection has failed and cannot be recovered should reconnect be enabled.long
drainTimeout()
ConnectionOptions
drainTimeout(long drainTimeout)
Sets the drain timeout (in milliseconds) after which aReceiver
request to drain link credit is considered failed and the request will be marked as such.ConnectionOptions
drainTimeout(long timeout, java.util.concurrent.TimeUnit units)
Sets the drain timeout value after which aReceiver
request to drain link credit is considered failed and the request will be marked as such.long
idleTimeout()
ConnectionOptions
idleTimeout(long idleTimeout)
Sets the idle timeout (in milliseconds) after which the connection will be closed if the peer has not send any data.ConnectionOptions
idleTimeout(long timeout, java.util.concurrent.TimeUnit units)
Sets the idle timeout value after which the connection will be closed if the peer has not send any data.java.util.function.BiConsumer<Connection,DisconnectionEvent>
interruptedHandler()
ConnectionOptions
interruptedHandler(java.util.function.BiConsumer<Connection,DisconnectionEvent> interruptedHandler)
Configures a handler that will be notified when the currentConnection
experiences an interruption.int
maxFrameSize()
ConnectionOptions
maxFrameSize(int maxFrameSize)
Sets the max frame size (in bytes), values of -1 indicates to use the client selected default.java.lang.String[]
offeredCapabilities()
ConnectionOptions
offeredCapabilities(java.lang.String... offeredCapabilities)
Sets the collection of capabilities to offer to the remote from a newConnection
created using theseConnectionOptions
.long
openTimeout()
ConnectionOptions
openTimeout(long openTimeout)
Configures the timeout used when awaiting a response from the remote that a request to open a resource such as aConnection
,Session
,Sender
orReceiver
has been honored.ConnectionOptions
openTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a response from the remote that a request to open a resource such as aConnection
,Session
,Sender
orReceiver
has been honored.java.lang.String
password()
ConnectionOptions
password(java.lang.String password)
Sets the password used when performing connection authentication.java.util.Map<java.lang.String,java.lang.Object>
properties()
ConnectionOptions
properties(java.util.Map<java.lang.String,java.lang.Object> properties)
Sets aMap
of properties to convey to the remote when a newConnection
is created from theseConnectionOptions
.java.util.function.BiConsumer<Connection,ConnectionEvent>
reconnectedHandler()
ConnectionOptions
reconnectedHandler(java.util.function.BiConsumer<Connection,ConnectionEvent> reconnectedHandler)
Configures a handler that will be notified when aConnection
that has previously experienced and interruption has been reconnected to a remote based on the reconnection configuration.boolean
reconnectEnabled()
ConnectionOptions
reconnectEnabled(boolean reconnectEnabled)
Controls if the connection will attempt to reconnect if unable to connect immediately or if an existing connection fails.ReconnectOptions
reconnectOptions()
long
requestTimeout()
ConnectionOptions
requestTimeout(long requestTimeout)
Configures the timeout used when awaiting a response from the remote that a request to perform some action such as starting a new transaction.ConnectionOptions
requestTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a response from the remote that a request to perform some action such as starting a new transaction.SaslOptions
saslOptions()
long
sendTimeout()
ConnectionOptions
sendTimeout(long sendTimeout)
Configures the timeout used when awaiting a send operation to complete.ConnectionOptions
sendTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a send operation to complete.boolean
sslEnabled()
ConnectionOptions
sslEnabled(boolean sslEnabled)
Controls if the connection will attempt to connect using a secure IO layer or not.SslOptions
sslOptions()
boolean
traceFrames()
ConnectionOptions
traceFrames(boolean traceFrames)
Configure if the newly created connection should enabled AMQP frame tracing to the system output.TransportOptions
transportOptions()
java.lang.String
user()
ConnectionOptions
user(java.lang.String user)
Sets the user name used when performing connection authentication.java.lang.String
virtualHost()
ConnectionOptions
virtualHost(java.lang.String virtualHost)
The virtual host value to provide to the remote when creating a newConnection
.
-
-
-
Field Detail
-
DEFAULT_DESIRED_CAPABILITIES
public static final java.util.List<java.lang.String> DEFAULT_DESIRED_CAPABILITIES
-
INFINITE
public static final long INFINITE
- See Also:
- Constant Field Values
-
DEFAULT_OPEN_TIMEOUT
public static final long DEFAULT_OPEN_TIMEOUT
- See Also:
- Constant Field Values
-
DEFAULT_CLOSE_TIMEOUT
public static final long DEFAULT_CLOSE_TIMEOUT
- See Also:
- Constant Field Values
-
DEFAULT_SEND_TIMEOUT
public static final long DEFAULT_SEND_TIMEOUT
- See Also:
- Constant Field Values
-
DEFAULT_REQUEST_TIMEOUT
public static final long DEFAULT_REQUEST_TIMEOUT
- See Also:
- Constant Field Values
-
DEFAULT_IDLE_TIMEOUT
public static final long DEFAULT_IDLE_TIMEOUT
- See Also:
- Constant Field Values
-
DEFAULT_DRAIN_TIMEOUT
public static final long DEFAULT_DRAIN_TIMEOUT
- See Also:
- Constant Field Values
-
DEFAULT_CHANNEL_MAX
public static final int DEFAULT_CHANNEL_MAX
- See Also:
- Constant Field Values
-
DEFAULT_MAX_FRAME_SIZE
public static final int DEFAULT_MAX_FRAME_SIZE
- See Also:
- Constant Field Values
-
DEFAULT_NEXT_RECEIVER_POLICY
public static final NextReceiverPolicy DEFAULT_NEXT_RECEIVER_POLICY
-
-
Constructor Detail
-
ConnectionOptions
public ConnectionOptions()
Create a newConnectionOptions
instance configured with default configuration settings.
-
ConnectionOptions
public ConnectionOptions(ConnectionOptions options)
Creates aConnectionOptions
instance that is a copy of the given instance.- Parameters:
options
- TheConnectionOptions
instance whose configuration should be copied to this one.
-
-
Method Detail
-
clone
public ConnectionOptions clone()
- Overrides:
clone
in classjava.lang.Object
-
copyInto
protected ConnectionOptions copyInto(ConnectionOptions other)
Copy all options from thisConnectionOptions
instance into the instance provided.- Parameters:
other
- the target of this copy operation.- Returns:
- this
ConnectionOptions
instance.
-
closeTimeout
public long closeTimeout()
- Returns:
- the timeout used when awaiting a response from the remote when a resource is closed.
-
closeTimeout
public ConnectionOptions closeTimeout(long closeTimeout)
Configures the timeout used when awaiting a response from the remote that a request to close a resource such as aConnection
,Session
,Sender
orReceiver
h as been honored.- Parameters:
closeTimeout
- Timeout value in milliseconds to wait for a remote response.- Returns:
- this
ConnectionOptions
instance.
-
closeTimeout
public ConnectionOptions closeTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a response from the remote that a request to close a resource such as aConnection
,Session
,Sender
orReceiver
h as been honored.- Parameters:
timeout
- Timeout value to wait for a remote response.units
- TheTimeUnit
that defines the timeout span.- Returns:
- this
ConnectionOptions
instance.
-
openTimeout
public long openTimeout()
- Returns:
- the timeout used when awaiting a response from the remote when a resource is opened.
-
openTimeout
public ConnectionOptions openTimeout(long openTimeout)
Configures the timeout used when awaiting a response from the remote that a request to open a resource such as aConnection
,Session
,Sender
orReceiver
has been honored.- Parameters:
openTimeout
- Timeout value in milliseconds to wait for a remote response.- Returns:
- this
ConnectionOptions
instance.
-
openTimeout
public ConnectionOptions openTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a response from the remote that a request to open a resource such as aConnection
,Session
,Sender
orReceiver
has been honored.- Parameters:
timeout
- Timeout value to wait for a remote response.units
- TheTimeUnit
that defines the timeout span.- Returns:
- this
ConnectionOptions
instance.
-
sendTimeout
public long sendTimeout()
- Returns:
- the timeout used when awaiting a response from the remote when a resource is message send.
-
sendTimeout
public ConnectionOptions sendTimeout(long sendTimeout)
Configures the timeout used when awaiting a send operation to complete. A send will block if the remote has not granted theSender
or theSession
credit to do so, if the send blocks for longer than this timeout the send call will fail with anClientSendTimedOutException
exception to indicate that the send did not complete.- Parameters:
sendTimeout
- Timeout value in milliseconds to wait for a remote response.- Returns:
- this
ConnectionOptions
instance.
-
sendTimeout
public ConnectionOptions sendTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a send operation to complete. A send will block if the remote has not granted theSender
or theSession
credit to do so, if the send blocks for longer than this timeout the send call will fail with anClientSendTimedOutException
exception to indicate that the send did not complete.- Parameters:
timeout
- Timeout value to wait for a remote response.units
- TheTimeUnit
that defines the timeout span.- Returns:
- this
ConnectionOptions
instance.
-
requestTimeout
public long requestTimeout()
- Returns:
- the timeout used when awaiting a response from the remote when a resource makes a request.
-
requestTimeout
public ConnectionOptions requestTimeout(long requestTimeout)
Configures the timeout used when awaiting a response from the remote that a request to perform some action such as starting a new transaction. If the remote does not respond within the configured timeout the resource making the request will mark it as failed and return an error to the request initiator usually in the form of aClientOperationTimedOutException
.- Parameters:
requestTimeout
- Timeout value in milliseconds to wait for a remote response.- Returns:
- this
ConnectionOptions
instance.
-
requestTimeout
public ConnectionOptions requestTimeout(long timeout, java.util.concurrent.TimeUnit units)
Configures the timeout used when awaiting a response from the remote that a request to perform some action such as starting a new transaction. If the remote does not respond within the configured timeout the resource making the request will mark it as failed and return an error to the request initiator usually in the form of aClientOperationTimedOutException
.- Parameters:
timeout
- Timeout value to wait for a remote response.units
- TheTimeUnit
that defines the timeout span.- Returns:
- this
ConnectionOptions
instance.
-
channelMax
public int channelMax()
- Returns:
- the configured or default channel max value for create
Connection
instances.
-
channelMax
public ConnectionOptions channelMax(int channelMax)
Configure the channel maximum value for the newConnection
created with these options.The channel max value controls how many
Session
instances can be created by a given Connection, the default value is 65535.- Parameters:
channelMax
- The channel max value to assign to newly createdConnection
instances.- Returns:
- this
ConnectionOptions
instance.
-
maxFrameSize
public int maxFrameSize()
- Returns:
- the configure maximum frame size value for newly create
Connection
instances.
-
maxFrameSize
public ConnectionOptions maxFrameSize(int maxFrameSize)
Sets the max frame size (in bytes), values of -1 indicates to use the client selected default.- Parameters:
maxFrameSize
- the frame size in bytes.- Returns:
- this
ConnectionOptions
instance.
-
idleTimeout
public long idleTimeout()
- Returns:
- the configured idle timeout value that will be sent to the remote.
-
idleTimeout
public ConnectionOptions idleTimeout(long idleTimeout)
Sets the idle timeout (in milliseconds) after which the connection will be closed if the peer has not send any data. The provided value will be halved before being transmitted as our advertised idle-timeout in the AMQPOpen
frame.- Parameters:
idleTimeout
- the timeout in milliseconds.- Returns:
- this
ConnectionOptions
instance.
-
idleTimeout
public ConnectionOptions idleTimeout(long timeout, java.util.concurrent.TimeUnit units)
Sets the idle timeout value after which the connection will be closed if the peer has not send any data. The provided value will be halved before being transmitted as our advertised idle-timeout in the AMQPOpen
frame.- Parameters:
timeout
- Timeout value to wait for a remote response.units
- TheTimeUnit
that defines the timeout span.- Returns:
- this
ConnectionOptions
instance.
-
drainTimeout
public long drainTimeout()
- Returns:
- the configured drain timeout value that will use to fail a pending drain request.
-
drainTimeout
public ConnectionOptions drainTimeout(long drainTimeout)
Sets the drain timeout (in milliseconds) after which aReceiver
request to drain link credit is considered failed and the request will be marked as such.- Parameters:
drainTimeout
- the drainTimeout to use for receiver links.- Returns:
- this
ConnectionOptions
instance.
-
drainTimeout
public ConnectionOptions drainTimeout(long timeout, java.util.concurrent.TimeUnit units)
Sets the drain timeout value after which aReceiver
request to drain link credit is considered failed and the request will be marked as such.- Parameters:
timeout
- Timeout value to wait for a remote response.units
- TheTimeUnit
that defines the timeout span.- Returns:
- this
ConnectionOptions
instance.
-
offeredCapabilities
public java.lang.String[] offeredCapabilities()
- Returns:
- the offeredCapabilities that have been configured.
-
offeredCapabilities
public ConnectionOptions offeredCapabilities(java.lang.String... offeredCapabilities)
Sets the collection of capabilities to offer to the remote from a newConnection
created using theseConnectionOptions
. The offered capabilities advertise to the remote capabilities that thisConnection
supports.- Parameters:
offeredCapabilities
- the offeredCapabilities to set on a newConnection
.- Returns:
- this
ConnectionOptions
instance.
-
desiredCapabilities
public java.lang.String[] desiredCapabilities()
- Returns:
- the desiredCapabilities that have been configured.
-
desiredCapabilities
public ConnectionOptions desiredCapabilities(java.lang.String... desiredCapabilities)
Sets the collection of capabilities to request from the remote for a newConnection
created using theseConnectionOptions
. The desired capabilities inform the remote peer of the various capabilities the newConnection
requires and the remote should return those that it supports in its offered capabilities.- Parameters:
desiredCapabilities
- the desiredCapabilities to set on a newConnection
.- Returns:
- this
ConnectionOptions
instance.
-
properties
public java.util.Map<java.lang.String,java.lang.Object> properties()
- Returns:
- the properties that have been configured.
-
properties
public ConnectionOptions properties(java.util.Map<java.lang.String,java.lang.Object> properties)
Sets aMap
of properties to convey to the remote when a newConnection
is created from theseConnectionOptions
.- Parameters:
properties
- the properties to set- Returns:
- this
ConnectionOptions
instance.
-
virtualHost
public java.lang.String virtualHost()
- Returns:
- the virtual host value configured.
-
virtualHost
public ConnectionOptions virtualHost(java.lang.String virtualHost)
The virtual host value to provide to the remote when creating a newConnection
.- Parameters:
virtualHost
- the virtual host to set- Returns:
- this
ConnectionOptions
instance.
-
user
public java.lang.String user()
- Returns:
- the user name that is configured for new
Connection
instances.
-
user
public ConnectionOptions user(java.lang.String user)
Sets the user name used when performing connection authentication.- Parameters:
user
- the user to set- Returns:
- this
ConnectionOptions
instance.
-
password
public java.lang.String password()
- Returns:
- the password that is configured for new
Connection
instances.
-
password
public ConnectionOptions password(java.lang.String password)
Sets the password used when performing connection authentication.- Parameters:
password
- the password to set- Returns:
- this
ConnectionOptions
instance.
-
transportOptions
public TransportOptions transportOptions()
- Returns:
- the transport options that will be used for the
Connection
.
-
sslOptions
public SslOptions sslOptions()
- Returns:
- the SSL options that will be used for the
Connection
.
-
saslOptions
public SaslOptions saslOptions()
- Returns:
- the SASL options that will be used for the
Connection
.
-
reconnectEnabled
public boolean reconnectEnabled()
- Returns:
- true if reconnection support has been enabled for this connection.
-
reconnectEnabled
public ConnectionOptions reconnectEnabled(boolean reconnectEnabled)
Controls if the connection will attempt to reconnect if unable to connect immediately or if an existing connection fails.This option enables or disables reconnection to a remote remote peer after IO errors. To control specifics of the reconnection configuration for the
Connection
the values must be updated in theReconnectOptions
configuration prior to creating the connection.- Parameters:
reconnectEnabled
- Controls if reconnection is enabled or not for the associatedConnection
.- Returns:
- this options instance.
-
reconnectOptions
public ReconnectOptions reconnectOptions()
- Returns:
- the reconnection options that will be used for the
Connection
.
-
traceFrames
public ConnectionOptions traceFrames(boolean traceFrames)
Configure if the newly created connection should enabled AMQP frame tracing to the system output.- Parameters:
traceFrames
- true if frame tracing on this connection should be enabled.- Returns:
- this
ConnectionOptions
instance.
-
traceFrames
public boolean traceFrames()
- Returns:
- true if the connection is configured to perform frame tracing.
-
sslEnabled
public boolean sslEnabled()
- Returns:
- true if SSL support has been enabled for this connection.
-
sslEnabled
public ConnectionOptions sslEnabled(boolean sslEnabled)
Controls if the connection will attempt to connect using a secure IO layer or not.This option enables or disables SSL encryption when connecting to a remote peer. To control specifics of the SSL configuration for the
Connection
the values must be updated in theSslOptions
configuration prior to creating the connection.- Parameters:
sslEnabled
- Is SSL encryption enabled for theConnection
.- Returns:
- this
ConnectionOptions
instance.
-
defaultNextReceiverPolicy
public NextReceiverPolicy defaultNextReceiverPolicy()
- Returns:
- the configured default next receiver policy for the connection.
-
defaultNextReceiverPolicy
public ConnectionOptions defaultNextReceiverPolicy(NextReceiverPolicy policy)
Configures the default next receiver policy for this connection and any session that is created without specifying user defined session default options.- Parameters:
policy
- The next receiver policy to assign as the default.- Returns:
- this
ConnectionOptions
instance.
-
disconnectedHandler
public java.util.function.BiConsumer<Connection,DisconnectionEvent> disconnectedHandler()
- Returns:
- the connection failed handler currently registered.
-
disconnectedHandler
public ConnectionOptions disconnectedHandler(java.util.function.BiConsumer<Connection,DisconnectionEvent> disconnectedHandler)
Configures a handler that will be notified when the connection has failed and cannot be recovered should reconnect be enabled. Once notified of the failure theConnection
is no longer operable and theConnection
APIs will throw an exception to indicate that the connection has failed. The client application should close a failedConnection
once it becomes aware of the failure to ensure all connection resources are cleaned up properly.- Parameters:
disconnectedHandler
- the connection failed handler to notify when the connection fails for any reason.- Returns:
- this
ConnectionOptions
instance. - See Also:
interruptedHandler
,connectedHandler
,disconnectedHandler
-
connectedHandler
public java.util.function.BiConsumer<Connection,ConnectionEvent> connectedHandler()
- Returns:
- the connection established handler that is currently registered
-
connectedHandler
public ConnectionOptions connectedHandler(java.util.function.BiConsumer<Connection,ConnectionEvent> connectedHandler)
Configures a handler that will be notified when aConnection
has established. This handler is called for each connection event when reconnection is enabled unless areconnectedHandler
is configured in which case this handler is only notified on the first connection to a remote.- Parameters:
connectedHandler
- the connection established handler to assign to theseConnectionOptions
.- Returns:
- this
ConnectionOptions
instance. - See Also:
disconnectedHandler()
,interruptedHandler
,reconnectedHandler
-
interruptedHandler
public java.util.function.BiConsumer<Connection,DisconnectionEvent> interruptedHandler()
- Returns:
- the connection interrupted handler that is currently registered
-
interruptedHandler
public ConnectionOptions interruptedHandler(java.util.function.BiConsumer<Connection,DisconnectionEvent> interruptedHandler)
Configures a handler that will be notified when the currentConnection
experiences an interruption. TheConnection
will only signal this handler when the reconnection feature is enabled and will follow this event either with a notification that the connection has been restored (if a handler is registered), or with a notification that the connection has failed if the reconnection configuration places limits on the the number of reconnection attempts.- Parameters:
interruptedHandler
- the connection interrupted handler to assign to theseConnectionOptions
.- Returns:
- this
ReconnectOptions
instance. - See Also:
connectedHandler
,reconnectedHandler
,disconnectedHandler
-
reconnectedHandler
public java.util.function.BiConsumer<Connection,ConnectionEvent> reconnectedHandler()
- Returns:
- the connection restored handler that is currently registered
-
reconnectedHandler
public ConnectionOptions reconnectedHandler(java.util.function.BiConsumer<Connection,ConnectionEvent> reconnectedHandler)
Configures a handler that will be notified when aConnection
that has previously experienced and interruption has been reconnected to a remote based on the reconnection configuration.- Parameters:
reconnectedHandler
- the connection restored handler to assign to theseConnectionOptions
.- Returns:
- this
ReconnectOptions
instance. - See Also:
connectedHandler
,interruptedHandler
,disconnectedHandler
-
-


Status Yellow low temperature warning issued for Mayo
A STATUS Yellow low temperature warning has been issued for Mayo.
It comes into effect at 8 p.m. today and remains in place until 9 a.m. tomorrow.
Met. Èireann is forecasting very cold conditions with minimum air temperatures ranging between minus two and minus four Celsius.
There will be widespread frost with the risk of icy patches in places.


Constructing ZF Set Theory in Agda
Menu Menu
ZF in Agda
zf.agda axiom of ZF zfc.agda axiom of choice Ordinals.agda axiom of Ordinals ordinal.agda countable model of Ordinals OD.agda model of ZF based on Ordinal Definable Set with assumptions ODC.agda Law of exclude middle from axiom of choice assumptions LEMC.agda model of choice with assumption of the Law of exclude middle OPair.agda ordered pair on OD BAlgbra.agda Boolean algebra on OD (not yet done) filter.agda Filter on OD (not yet done) cardinal.agda Caedinal number on OD (not yet done) logic.agda some basics on logic nat.agda some basics on Nat
Programming Mathematics
Programming is processing data structure with λ terms.
We are going to handle Mathematics in intuitionistic logic with λ terms.
Mathematics is a functional programming which values are proofs.
Programming ZF Set Theory in Agda
Target
Describe ZF axioms in Agda Construction a Model of ZF Set Theory in Agda Show necessary assumptions for the model Show validities of ZF axioms on the modelThis shows consistency of Set Theory (with some assumptions), without circulating ZF Theory assumption.
ZF in Agda https://github.com/shinji-kono/zf-in-agda
Why Set Theory
If we can formulate Set theory, it suppose to work on any mathematical theory.Set Theory is a difficult point for beginners especially axiom of choice.

I'm planning to do it in my old age, but I'm enough age now.
if you familier with Agda, you can skip to there
Agda and Intuitionistic Logic
Curry Howard Isomorphism
Proposition : Proof ⇔ Type : Valuewhich means
constructing a typed lambda calculus which corresponds a logic
Typed lambda calculus which allows complex type as a value of a variable (System FC)
First class Type / Dependent Type
Agda is a such a programming language which has similar syntax of Haskell
Coq is specialized in proof assistance such as command and tactics .
Introduction of Agda
A length of a list of type A.
length : {A : Set } → List A → Nat length [] = zero length (_ ∷ t) = suc ( length t )Simple functional programming language. Type declaration is mandatory. A colon means type, an equal means value. Indentation based.
Set is a base type (which may have a level ).
{} means implicit variable which can be omitted if Agda infers its value.
data ( Sum type )
A data type which as exclusive multiple constructors. A similar one as union in C or case class in Scala.It has a similar syntax as Haskell but it has a slight difference.
data List (A : Set ) : Set where [] : List A _∷_ : A → List A → List A_∷_ means infix operator. If use explicit _, it can be used in a normal function syntax.
Natural number can be defined as a usual way.
data Nat : Set where zero : Nat suc : Nat → Nat
A → B means "A implies B"
In Agda, a type can be a value of a variable, which is usually called dependent type. Type has a name Set in Agda.
ex3 : {A B : Set} → Set ex3 {A}{B} = A → Bex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
A type is a formula, the value is the proofA value of A → B can be interpreted as an inference from the formula A to the formula B, which can be a function from a proof of A to a proof of B.
introduction と elimination
For a logical operator, there are two types of inference, an introduction and an elimination.
intro creating symbol / constructor / introduction elim using symbolic / accessors / eliminationIn Natural deduction, this can be written in proof schema.
A : B A A → B ------------- →intro ------------------ →elim A → B BIn Agda, this is a pair of type and value as follows. Introduction of → uses λ.
→intro : {A B : Set } → A → B → ( A → B ) →intro _ b = λ x → b →elim : {A B : Set } → A → ( A → B ) → B →elim a f = f aImportant
{A B : Set } → A → B → ( A → B )is
{A B : Set } → ( A → ( B → ( A → B ) ))This makes currying of function easy.
To prove A → B
Make a left type as an argument. (intros in Coq)
ex5 : {A B C : Set } → A → B → C → ? ex5 a b c = ?? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red), insufficient proof or instance (Yellow), Non-termination, the proof is completed.
A ∧ B
Well known conjunction's introduction and elimination is as follow.
A B A ∧ B A ∧ B ------------- ----------- proj1 ---------- proj2 A ∧ B A BWe can introduce a corresponding structure in our functional programming language.
record
record _∧_ A B : Set field proj1 : A proj2 : B_∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) )
This a type which constructed from type A and type B. You may think this as an object or struct.
record { proj1 = x ; proj2 = y }is a constructor of _∧_.
ex3 : {A B : Set} → A → B → ( A ∧ B ) ex3 a b = record { proj1 = a ; proj2 = b } ex1 : {A B : Set} → ( A ∧ B ) → A ex1 a∧b = proj1 a∧ba∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols except parenthesis or colons. A symbol requires space separation such as a type defining colon.
Defining record can be recursively, but we don't use the recursion here.
Mathematical structure
We have types of elements and the relationship in a mathematical structure.
logical relation has no ordering there is a natural ordering in arguments and a value in a functionSo we have typical definition style of mathematical structure with records.
record IsOrdinals {n : Level} (ord : Set n) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where field Otrans : {x y z : ord } → x o< y → y o< z → x o< z record Ordinals {n : Level} : Set (suc (suc n)) where field ord : Set n _o<_ : ord → ord → Set n isOrdinal : IsOrdinals ord _o<_In IsOrdinals, axioms are written in flat way. In Ordinal, we may have inputs and outputs are put in the field including IsOrdinal.
Fields of Ordinal is existential objects in the mathematical structure.
Limit Ordinal
If an ordinal is not a succesor of other, it is called limit ordinal. We need predicate to decide it.
not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))An ordinal may have an imeditate limit ordinal, we call it next x. Axiom of nrext is this.
record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field x<nx : { y : ord } → (y o< next y ) osuc<nx : { x y : ord } → x o< next y → osuc x o< next y ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))We show some intresting lemma.
next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)These are proved from the axiom. Our countable ordinal satisfies these.
A Model and a theory
Agda record is a type, so we can write it in the argument, but is it really exists?If we have a value of the record, it simply exists, that is, we need to create all the existence in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
type of record = theory value of record = modelWe call the value of the record as a model. If mathematical structure has a model, it exists. Pretty Obvious.
postulate と module
Agda proofs are separated by modules, which are large records.postulates are assumptions. We can assume a type without proofs.
postulate sup-o : ( Ordinal → Ordinal ) → Ordinal sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψsup-o is an example of upper bound of a function and sup-o< assumes it actually satisfies all the value is less than upper bound.
Writing some type in a module argument is the same as postulating a type, but postulate can be written the middle of a proof.
postulate can be constructive.
postulate can be inconsistent, which result everything has a proof. Actualy this assumption doesnot work for Ordinals, we discuss this later.
A ∨ B
data _∨_ (A B : Set) : Set where case1 : A → A ∨ B case2 : B → A ∨ BAs Haskell, case1/case2 are patterns.
ex3 : {A B : Set} → ( A ∨ A ) → A ex3 = ?In a case statement, Agda command C-C C-C generates possible cases in the head.
ex3 : {A B : Set} → ( A ∨ A ) → A ex3 (case1 x) = ? ex3 (case2 x) = ?Proof schema of ∨ is omit due to the complexity.
Negation
⊥ ------------- ⊥-elim AAnything can be derived from bottom, in this case a Set A. There is no introduction rule in ⊥, which can be implemented as data which has no constructor.
data ⊥ : Set where⊥-elim can be proved like this.
⊥-elim : {A : Set } -> ⊥ -> A ⊥-elim ()() means no match argument nor value.
A negation can be defined using ⊥ like this.
¬_ : Set → Set ¬ A = A → ⊥
Equality
All the value in Agda are terms. If we have the same normalized form, two terms are equal. If we have variables in the terms, we will perform an unification. unifiable terms are equal. We don't go further on the unification.
{ x : A } x ≡ y f x y --------------- ≡-intro --------------------- ≡-elim x ≡ x f x xequality _≡_ can be defined as a data.
data _≡_ {A : Set } : A → A → Set where refl : {x : A} → x ≡ xThe elimination of equality is a substitution in a term.
subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y subst {A} {x} {y} f refl fx = fx ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
Equivalence relation
refl' : {A : Set} {x : A } → x ≡ x refl' = ? sym : {A : Set} {x y : A } → x ≡ y → y ≡ x sym = ? trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z trans = ? cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y cong = ?
Ordering
Relation is a predicate on two value which has a same type.
A → A → SetDefining order is the definition of this type with predicate or a data.
data _≤_ : Rel ℕ 0ℓ where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
Quantifier
Handling quantifier in an intuitionistic logic requires special cares.
In the input of a function, there are no restriction on it, that is, it has a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
There is no ∃ in agda, the one way is using negation like this.
∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) )
On the another way, f : A can be used like this.
p fIf we use a function which can be defined globally which has stronger meaning the usage of ∃ x in a logical expression.
Can we do math in this way?
Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
define mathematical structure as a record program inferences as if we have proofs in variables
Things which Agda cannot prove
The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which leads uniqueness of a functor in Category Theory.
Functional extensionality cannot be proved.
(∀ x → f x ≡ g x) → f ≡ gAgda has no law of exclude middle.
a ∨ ( ¬ a )For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
It also other problems such as termination, type inference or unification which we may overcome with efforts or devices or may not.
If we cannot prove something, we can safely postulate it unless it leads a contradiction.
Classical story of ZF Set Theory
Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads
a relative consistency proof of the Set Theory.
Ordinal number is used in the flow.
In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
We need some non constructive assumptions in the construction. A model of Set theory is
constructed based on these assumptions.
Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
which is not a successor of any ordinals. It is called limit ordinal.
Any two ordinal can be compared, that is less, equal or more, that is total order.
We can define a list like structure with level, which is a kind of two dimensional infinite array.
It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
So our Ordinals has a mode. This means axiom of Ordinals are consistent.
If not, we may fix the axioms or the model, such as the definitions of the order.
We can also ask whether the inputs exist.
If we handle real-number in the model, only countable number of real-number is used.
We don't show the definition of cardinal number here.
From naive point view, a set i a list, but in Agda, elements have all the same type.
A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
Finite set may be written in finite series of ∨, but ...
This operation can be performed within a ZF Set theory. Classical Set Theory assumes
ZF, so this kind of thing is allowed.
But in our case, we have no ZF theory, so we are going to use Ordinals.
The idea is to use an ordinal as a pointer to a record which defines a Set.
If the recored defines a series of Ordinals which is a pointer to the Set. This record looks like a Set.
This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself.
A ∋ x can be define as follows.
We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
ZF axioms in Agda.
It may not valid in our model. We have to debug it.
Fixes are depends on axioms.
≡ is an equality of λ terms, but please not that this is equality on Ordinals.
Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
But we haven't defined == yet.
Axiom of Extensionality requires sets having the same elements are handled in the same way
each other.
x == y can be defined in this way.
Actual proof is rather complicated.
To prove extensionality or other we need ==→o≡.
Since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
We can calculate the minimum using sup if we have bound but it is tedius.
Only Select has non minimum odmax. We have the same problem on 'def' itself, but we leave it, that is we assume the
assumption of predicates of Agda have a unique form, it is something like the
functional extensionality assumption.
It means it has ω as a ZF Set. It is ususally written like this.
To define an OD which arrows & (Union (x , (x , x))) as a predicate, we can use Agda data structure.
We have large freedom on HOD. We reqest no minimality on odmax, so it may arbitrary larger.
The address of HOD can be larger at least it have to be larger than the content's address.
We only have a relative ordering such as
In other words, the space between address of HOD and its bound is arbitrary, it is possible to assume ω has no bound.
This is the reason of necessity of Axiom of infinite.
Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
Power Set axiom requires double negation,
Proof of validity is straight forward.
Once we have a bound, validity of the axiom is an easy task to check the logical relation-ship.
Axiom of regularity requires non self intersectable elements (which is called minimum), if we
replace it by a function, it becomes a choice function. It makes axiom of choice valid.
This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
choice also becomes valid.
The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) .
The cumulative hierarchy
If we assumes excluded middle, these are exactly same.
Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
Except the upper bound, axioms are simple logical relation.
Proof of existence of mapping between HOD and Ordinals are not obvious. We don't know we prove it or not.
Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
but we don't have explicit upper limit on Ordinals.
Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
ZF record itself is not necessary, for example, topology theory without ZF can be possible.
Topos itself is model of intuitionistic logic.
Transitive Sets are objects of Cartesian closed category.
It is possible to introduce Power Set Functor on it
We can use replacement A ∩ x for each element in Transitive Set,
in the similar way of our power set axiom. I
A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus.
Our Agda model is a proof theoretic version of it.
definition of cardinal number is not yet done
definition of filter is not yet done
we may have a model without axiom of choice or without continuum hypothesis
Possible representation of continuum hypothesis is this.
filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
is depends on axiom of choice.
This may be simpler than classical forcing theory ( not yet done).
Type inference and termination is not so clear in multi recursions.
Defining Agda record is a good way to understand mathematical theory, for examples,
Ordinals
Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
It also has a successor osuc.
record Ordinals {n : Level} : Set (suc (suc n)) where
field
ord : Set n
o∅ : ord
osuc : ord → ord
_o<_ : ord → ord → Set n
isOrdinal : IsOrdinals ord o∅ osuc _o<_
It is different from natural numbers in way. The order of Ordinals is not defined in terms
of successor. It is given from outside, which make it possible to have higher order infinity.
Axiom of Ordinals
Properties of infinite things. We request a transfinite induction, which states that if
some properties are satisfied below all possible ordinals, the properties are true on all
ordinals.
record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord )
(osuc : ord → ord )
(_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
field
Otrans : {x y z : ord } → x o< y → y o< z → x o< z
OTri : Trichotomous {n} _≡_ _o<_
¬x<0 : { x : ord } → ¬ ( x o< o∅ )
<-osuc : { x : ord } → x o< osuc x
osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
TransFinite : { ψ : ord → Set (suc n) }
→ ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
→ ∀ (x : ord) → ψ x
Concrete Ordinals or Countable Ordinals
data OrdinalD {n : Level} : (lv : Nat) → Set n where
Φ : (lv : Nat) → OrdinalD lv
OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
The order of the OrdinalD can be defined in this way.
data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
This is a simple data structure, it has no abstract assumptions, and it is countable many data
structure.
Φ 0
OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
Osuc 0 (Φ 0) d< Φ 1
Model of Ordinals
Debugging axioms using Model
Whether axiom is correct or not can be checked by a validity on a mode.
Countable Ordinals can contains uncountable set?
Yes, the ordinals contains any level of infinite Set in the axioms.
from the outside view point, it is countable
from the internal view point, it is uncountable
The definition of countable/uncountable is the same, but the properties are different
depending on the context.
What is Set
The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
We don't ask the contents of Set. It can be anything.
From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
and all of them, and again we repeat this.
φ {φ} {φ,{φ}}, {φ,{φ},...}
It is called V.
Ordinal Definable Set
We can define a sbuset of Ordinals using predicates.  In Agda, OD is defined as follows.
record OD : Set (suc n ) where
field
def : (x : Ordinal ) → Set n
Ordinals itself is not a set in a ZF Set theory but a class. In OD,
data One : Set n where
OneObj : One
record { def = λ x → One }
means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set.
You can say OD is a class in ZF Set Theory term.
OD is not ZF Set
If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like
a Set. The idea is to use an ordinal as a pointer to OD.
Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like
¬OD-order : ( & : OD → Ordinal )
→ ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥
¬OD-order & * c<→o< = ?
Actualy we can prove this contrdction, so we need some restrctions on OD.
HOD : Hereditarily Ordinal Definable
What we need is a bounded OD, the containment is limited by an ordinal.
record HOD : Set (suc n) where
field
od : OD
odmax : Ordinal
<odmax : {y : Ordinal} → def od y → y o< odmax
In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
HOD = { x | TC x ⊆ OD }
TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD.
1 to 1 mapping between an HOD and an Ordinal
HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
& : HOD → Ordinal
* : Ordinal → HOD
oiso : {x : HOD } → * ( & x ) ≡ x
diso : {x : Ordinal } → & ( * x ) ≡ x
we can check an HOD is an element of the OD using def.
_∋_ : ( A x : HOD ) → Set n
_∋_ A x = def (od A) ( & x )
In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
A x = def A ( & x ) = ψ (& x)
They say the existing of the mappings can be proved in Classical Set Theory, but we
simply assumes these non constructively.
Order preserving in the mapping of OD and Ordinal
Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ).
def (od y) ( & x )
An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
have to be smaller than the corresponding ordinal of the containing OD.
We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y
⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
If wa assumes reverse order preservation,
o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (* y) x
∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
Various Sets
In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
Ordinal / things satisfies axiom of Ordinal / extension of natural number
V / hierarchical construction of Set from φ
L / hierarchical predicate definable construction of Set from φ
HOD / Hereditarily Ordinal Definable
OD / equational formula on Ordinals
Agda Set / Type / it also has a level
Fixing ZF axom to fit intuitionistic logic
Pure logical axioms
empty, pair, select, ε-induction??infinity
These are logical relations among OD.
empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
infinity∅ : ∅ ∈ infinite
infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite
ε-induction : { ψ : OD → Set (suc n)}
→ ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
→ (x : OD ) → ψ x
finitely can be define by Agda data.
data infinite-d : ( x : Ordinal ) → Set n where
iφ : infinite-d o∅
isuc : {x : Ordinal } → infinite-d x →
infinite-d (& ( Union (* x , (* x , * x ) ) ))
Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
Axiom of Pair
In the Tanaka's book, axiom of pair is as follows.
∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
We have fix ∃ z, a function (x , y) is defined, which is _,_ .
_,_ : ( A B : ZFSet ) → ZFSet
using this, we can define two directions in separates axioms, like this.
pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
This is already written in Agda, so we use these as axioms. All inputs have ∀.
pair in OD
OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
_,_ : HOD → HOD → HOD
x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = ? ; <odmax = ? }
It is easy to find out odmax from odmax of x and y.
Validity of Axiom of Pair
Assuming ZFSet is OD, we are going to prove pair→ .
pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
pair→ x y t p = ?
In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ & x ) ∨ ( t ≡ & y ) .
pair→ x y t (case1 t≡x ) = ?
pair→ x y t (case2 t≡y ) = ?
The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ .
pair→ x y t (case1 t≡x ) = case1 ?
pair→ x y t (case2 t≡y ) = case2 ?
The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
which type is
t≡x : & t ≡ & x
which is shown by an Agda command (C-C C-E : agda2-show-context ).
Equality of OD and Axiom of Extensionality
OD is defined by a predicates, if we compares normal form of the predicates, even if
it contains the same elements, it may be different, which is no good as an equality of
Sets.
∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
We can write this axiom in Agda as follows.
extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
A ∈ w ⇔ B ∈ w from A == B.
record _==_ ( a b : OD ) : Set n where
field
eq→ : ∀ { x : Ordinal } → def a x → def b x
eq← : ∀ { x : Ordinal } → def b x → def a x
Actually, (z : HOD) → (A ∋ z) ⇔ (B ∋ z) implies od A == od B.
extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → od A == od B
eq→ (extensionality0 {A} {B} eq ) {x} d = ?
eq← (extensionality0 {A} {B} eq ) {x} d = ?
? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (* x))) d
eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (* x))) d
where
odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y → (def A (od y) → def (od B) y) → def (od A) x → def (od B) x
odef-iso refl t = t
The uniqueness of HOD
Validity of Axiom of Extensionality
If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes
==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
Using this, we have
extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
Axiom of infinity
∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
x ∪ { x } is Union (x , (x , x)) in our notation. It contains existential quantifier, so we introduce a function
infinite : ZFSet
infinity∅ : ∅ ∈ infinite
infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
ω in HOD
data infinite-d : ( x : Ordinal ) → Set n where
iφ : infinite-d o∅
isuc : {x : Ordinal } → infinite-d x →
infinite-d (& ( Union (* x , (* x , * x ) ) ))
It has simular structure as Data.Nat in Agda, and it defines a correspendence of HOD and the data structure. Now
we can define HOD like this.
infinite : HOD
infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ? ; <odmax = ? }
So what is the bound of ω? Analyzing the definition, it depends on the value of & (x , x), which
cannot know the aboslute value. This is because we don't have constructive definition of & : HOD → Ordinal.
HOD and Agda data structure
We may have
a HOD <=> Agda Data Strucure
as a data in Agda. Ex.
data ord-pair : (p : Ordinal) → Set n where
pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
ZFProduct : OD
ZFProduct = record { def = λ x → ord-pair x }
pi1 : { p : Ordinal } → ord-pair p → Ordinal
pi1 ( pair x y) = x
π1 : { p : HOD } → def ZFProduct (& p) → HOD
π1 lt = * (pi1 lt )
p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x
p-iso {x} p = ord≡→≡ (op-iso p)
HOD Ordrinal mapping
pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y)
Basicaly, we cannot know the concrete address of HOD other than empty set.
Possible restriction on HOD
We need some restriction on the HOD-Ordinal mapping. Simple one is this.
ωmax : Ordinal
<ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
It depends on infinite-d and put no assuption on the other similar construction. A more general one may be
hod-ord< : {x : HOD } → Set n
hod-ord< {x} = & x o< next (odmax x)
next : Ordinal → Ordinal means imediate next limit ordinal of x. It supress unecessary space between address of HOD and
its bound.
increment pase of address of HOD
Assuming, hod-ord< , we have
pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where
lemmab0 : next (odmax (x , x)) ≡ next (& x)
So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove
infinite-bound : ({x : HOD} → & x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
We also notice that if we have & (x , x) ≡ osuc (& x), c<→o< can be drived from ⊆→o≤ .
⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
→ ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
→ {x y : HOD } → def (od y) ( & x ) → & x o< & y
Non constructive assumptions so far
& : HOD → Ordinal
* : Ordinal → HOD
c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y
⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
oiso : {x : HOD } → * ( & x ) ≡ x
diso : {x : Ordinal } → & ( * x ) ≡ x
==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
Axiom which have negation form
Union, Selection
These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x )
power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t
If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
Union
The original form of the Axiom of Union is
∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃.
union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
The definition of Union in HOD is like this.
Union : HOD → HOD
Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) }
; odmax = osuc (& U) ; <odmax = ? }
The bound of Union is evident, but its proof is rather complicated.
union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
union→ X z u xx not = ⊥-elim ( not (& u) ( record { proj1 = proj1 xx
; proj2 = subst ( λ k → odef k (& z)) (sym oiso) (proj2 xx) } ))
union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
union← X z UX∋z = FExists _ lemma UX∋z where
lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
lemma {y} xx not = not (* y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
where
FExists : {m l : Level} → ( ψ : Ordinal → Set m )
→ {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
→ (exists : ¬ (∀ y → ¬ ( ψ y ) ))
→ ¬ p
FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
which checks existence using contra-position.
Axiom of replacement
We can replace the elements of a set by a function and it becomes a set. From the book,
∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
The existential quantifier can be related by a function,
Replace : HOD → (HOD → HOD ) → HOD
The axioms becomes as follows.
replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ
replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) )
In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
negation form of existential quantifier in the definition.
in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ & (ψ (* y ))))) }
in-codomain is a logical relation-ship, and it is written in OD.
Replace : HOD → (HOD → HOD) → HOD
Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x }
; odmax = rmax ; <odmax = rmax<} where
rmax : Ordinal
rmax = sup-o X (λ y X∋y → & (ψ (* y)))
rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
rmax< lt = proj1 lt
The bbound of Replace is defined by supremum, that is, it is not limited in a limit ordinal of original ZF Set.
Validity of Power Set Axiom
The original Power Set Axiom is this.
∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
The existential quantifier is replaced by a function
Power : ( A : OD ) → OD
t ⊆ X is a record like this.
record _⊆_ ( A B : OD ) : Set (suc n) where
field
incl : { x : OD } → A ∋ x → B ∋ x
Axiom becomes likes this.
power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
The validity of the axioms are slight complicated, we have to define set of all subset. We define
subset in a different form.
ZFSubset : (A x : HOD ) → HOD
ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where
lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
We can prove,
( {y : HOD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A )
We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
which is an Ordinals with our Model.
Ord : ( a : Ordinal ) → OD
Ord a = record { def = λ y → y o< a }
Def : (A : OD ) → OD
Def A = Ord ( sup-o ( λ x → & ( ZFSubset A (* x )) ) )
This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
Power : OD → OD
Power A = Replace (Def (Ord (& A))) ( λ x → A ∩ x )
Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → od a == od ( b ∩ a )
In case of Ord a intro of Power Set axiom becomes valid.
ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
Using this, we can prove,
power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
Axiom of regularity, Axiom of choice, ε-induction
minimal : (x : HOD ) → ¬ (x == od∅ )→ OD
x∋minimal : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → def x ( & ( minimal x ne ) )
minimal-1 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( def (minimal x ne) (& y)) ∧ (def x (& y) )
We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
ε-induction : { ψ : HOD → Set (suc n)}
→ ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
→ (x : HOD ) → ψ x
In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
We can formulate like this.
choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
It does not requires ∅ ∉ X .
Axiom of choice and Law of Excluded Middle
In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
but it requires law of the exclude middle.
ppp : { p : Set n } { a : HOD } → record { def = λ x → p } ∋ a → p
ppp {p} {a} d = d
We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
and Law of Excluded Middle is equivalent in our mode.
Relation-ship among ZF axiom
Non constructive assumption in our model
mapping between HOD and Ordinals
& : HOD → Ordinal
* : Ordinal → OD
oiso : {x : HOD } → * ( & x ) ≡ x
diso : {x : Ordinal } → & ( * x ) ≡ x
c<→o< : {x y : HOD } → def y ( & x ) → & x o< & y
⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
Equivalence on OD
==→o≡ : { x y : HOD } → (od x == od y) → x ≡ y
Upper bound
sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
In order to have bounded ω,
hod-ord< : {x : HOD} → & x o< next (odmax x)
Axiom of choice and strong axiom of regularity.
minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
V
V 0 := ∅
V α + 1 := P ( V α )
V α := ⋃ { V β | β < α }
Using TransFinite induction
V : ( β : Ordinal ) → HOD
V β = TransFinite V1 β where
V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
V1 x V0 with trio< x o∅
V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
V1 x V0 | tri> ¬a ¬b c with Oprev-p x
V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
V1 x V0 | tri> ¬a ¬b c | no ¬p =
record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ;
odmax = x; <odmax = λ {x} lt → proj1 lt }
In our system, clearly V ⊆ HOD。
L
The constructible Sets
L 0 := ∅
L α + 1 := Df (L α) -- Definable Power Set
V α := ⋃ { L β | β < α }
What is Df? In our system, Power x is definable by Sup.
record Definitions : Set (suc n) where
field
Definition : HOD → HOD
open Definitions
Df : Definitions → (x : HOD) → HOD
Df D x = Power x ∩ Definition D x
L
L : ( β : Ordinal ) → Definitions → HOD
L β D = TransFinite L1 β where
L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
L1 x L0 with trio< x o∅
L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
L1 x L0 | tri> ¬a ¬b c with Oprev-p x
L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
L1 x L0 | tri> ¬a ¬b c | no ¬p =
record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ;
odmax = x; <odmax = λ {x} lt → proj1 lt }
V=L
V=L0 : Set (suc n)
V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y }
is obvious. Definitions should have some restrictions, such as it includes Nat.
Some other ...
So it this correct?
Our axiom are syntactically the same in the text book, but negations are slightly different.
How to use Agda Set Theory
Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
postulated or assuming law of excluded middle.
Topos and Set Theory
Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
sub-object classifier.
Cardinal number and Continuum hypothesis
Axiom of choice is required to define cardinal number
continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
Filter
record Filter ( L : HOD ) : Set (suc n) where
field
filter : OD
proper : ¬ ( filter ∋ od∅ )
inL : filter ⊆ L
filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
We may construct a model of non standard analysis or set theory.
Programming Mathematics
Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
structure are
record and data
Proof is check by type consistency not by the computation, but it may include some normalization.
Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
Automaton ( Subset construction、Language containment)
are proved in Agda.
link
Summer school of foundation of mathematics (in Japanese)
https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/
Foundation of axiomatic set theory (in Japanese)
https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
Agda
https://agda.readthedocs.io/en/v<IP_ADDRESS>/
ZF-in-Agda source
https://github.com/shinji-kono/zf-in-agda.git
Category theory in Agda source
https://github.com/shinji-kono/category-exercise-in-agda


| | Household population1 | Communal Establishment Residents |
| | Males | Females | Males | Females |
| Marital Status | | | | |
| Single2 | 37.5 | 30.6 | 75.7 | 54.1 |
| Married3 | 49.1 | 46.2 | 9.1 | 6.2 |
| Separated or divorced4 | 10.2 | 13.2 | 7.2 | 3.6 |
| Widowed5 | 3.2 | 10.0 | 8.1 | 36.1 |
| Total | 100 | 100 | 100 | 100 |
| |
| Table Source: Office for National Statistics |
| |
| Notes: |
| 1. Household population includes 65,000 Communal Establishment staff or owners or family members or partners of staff or owners, to enable analysis of marital status by gender for residents as this data was not available for staff or owners (or family members or partners of staff or owners). |
| 2. Single (never married or never in a civil partnership). |
| 3. Married (including those in civil partnerships). |
| 4. Separated (but still legally married or in a civil partnership) or Divorced (including formerly in a civil partnership which is now legally dissolved). |
| 5. Widowed (including surviving partner from a civil partnership). |
| 6. Data from Census tables DC1116EWla and DC1107EW via Nomis. |


Child: Mom, can you tell me a bedtime story?
Me: Of course. *clears throat* Boy toy named Troy used to live in Detroit. Big dope dealer money, he was getting some coins. Was in shootouts with the law, but he live in a palace. Bought me Alexander McQueen, he was keeping me stylish.


A static site showcasing my AllOurData comps project.
Cole Hanson, Aishee Mukherji Jeffrey Boitnott Eric Odoom Yasmeen Awad
Coming Soon...


REPORT: Tua Tagovailoa’s Hip Injury Is Very Serious, “Similar To Bo Jackson’s Career-Ending Injury”
by Howard CosmellAfter a blow-out 38-7 win over Mississippi State on Saturday it is now being reported that Tua Tagovailoa’s hip injury is very serious. Some are even comparing it to the one that ended Bo Jackson’s career.
Dr. Mark Adickes took to twitter and tweeted out the following.
Nick Saban had this to say:
“I really don’t know at this point. We’ve got to do some MRIs and some things, but it’s a hip injury and that’s probably something that could be serious. So we just have to wait and see,” Saban said. (NBC SPORTS)
Cameras outside Davis Wade Stadium at Scott Field photograpged Tua being airlifted to St Vincent via helicopter.
This is not good news. Let’s pray that Tua makes a speedy recovery.
PRAYERS UP!!!


Obtaining an SMT Node
The get_smt command converts a symbol or an instance to an SMT node that corresponds to that symbol’s definition or the span of source represented by the instance.
get_smt
get_smt symbol|instance
Returns the SMT node that spans symbol or instance.
Note: The data command—which converts between symbols, instances, AST nodes, and data nodes—is not used to convert to or from SMT nodes.


About Me
I am a second-year Masters’ student at Brown University studying Biostatistics. My interest is in statistical learning and network meta-analysis. I am advised by Dr. Schmid Christophor.
I am a tennis enthusiast. My favorite player is Roger Federer, now and always!!!
Work Experience
I have worked for a BioTech Startup BrainCo as a machine learning engineer Intern. In that role, I built machine learning pipeline to process and make prediction on large-scale EEG data.
Projects
Skills
- Programming: Python, SQL, R, Julia
- Platforms: Tensorflow, Keras, Scikit-learn, Tableau, Plotly, Google Cloud Platform
- Specializations: Machine Learning, Deep Learning, NLP, A/B Test, Visualization
Selected Coursework
Computer Science
- Data Structure & Algorithms, Machine Learning, Deep Learning
Statistics
- Statistical Learning and Big Data, Statistical Inference, Practical Data Analysis
Applied Math
- Numerical Optimization


SWISH is inspired by web-based tools such as JSFIDDLE in that it allows you to develop a program and then share it with others on the Web. Besides sharing basic Prolog code fragments, we see several opportunities for deploying SWISH:
SWISH works fine recent versions of in Safari, Firefox, Chrome and Internet Explorer (tested IE 11).
SWISH can be added easily to any SWI-Prolog web application. For example, it is available as an extension pack for ClioPatria, the SWI-Prolog RDF framework. It can be added to ClioPatria using the command below, providing an alternative for SPARQL for exploring the database (requires SWI-Prolog 7.1.32 or later).
?- cpack_install(swish).
SWISH is implemented as a set of jQuery plugins, using Bootstrap for menus, modal windows and various styling aspects. SWISH uses CodeMirror for editing the Prolog source and query. Queries are executed by sending both the source text (left editor) and query (bottom-right editor) to the server, which creates a Pengine (Prolog Engine) to execute the query.
Pengines have many other applications, such as supporting Prolog RPC (Remote Procedure Calls, which allows you to execute a query fully transparent, including backtracking, on a remote server. An interesting aspect is that they provide a generic query language on top of an arbitrary Prolog program that can be used from JavaScript. A demo is available
The source code for SWISH is available on GitHub.


Lorem ipsum dolor sit amet consectetur adipisicing elit. Earum optio dolores repellendus quia cupiditate dicta reiciendis placeat autem quae porro deserunt quas voluptatem unde omnis quis, dolore fuga ab illo!
Helping people transition from prison and re-enter the community by providing better access to meaningful career opportunities, matching open positions and their skill set.
Helping local businesses fill skilled positions, and understand the state and federal benefits available to companies that hire people who have gone through the correctional system.
Helping the community by providing a service that helps reduce recidivism rates, in turn lowering rates of homelessness and extreme poverty.
"The benefits of prison education go beyond lowering recidivism rates and increasing post-release employment. It can also rekindle a sense of purpose and confidence."
teamwork
communication
leadership
technical training
"We've launched a coding program at San Quentin and we have a CAD program at Folsom Women's Facility here in Folsom," says Patillo. "And, they've invested money in those two programs to expand those to Pelican Bay, where we'll do coding and CAD, as well as the juvenile facility where they'll do coding in Ventura."
forklift operation
construction
culinary
Lorem ipsum dolor sit amet consectetur adipisicing elit.  Earum optio dolores repellendus quia cupiditate dicta reiciendis placeat autem quae porro deserunt quas voluptatem unde omnis quis, dolore fuga ab illo!
firefighting
Firefighting, along with less life-threatening trades like plumbing, welding, and cosmetology, is one of several vocational training programs offered to prisoners by the California Department of Corrections and Rehabilitation.
But once inmates leave prison, they often can’t work as firefighters, despite their frontline experience. In California, nearly all counties require firefighters to become licensed emergency medical technician (EMTs) — a credential that can be denied to almost anyone with a criminal record. - Nick Sibilla, USA Today
machining
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Proin ornare magna eros, eu pellentesque tortor vestibulum ut.
skilled labor
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Proin ornare magna eros, eu pellentesque tortor vestibulum ut. Maecenas non massa sem. Etiam finibus odio quis feugiat facilisis.
metal fabrication
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Proin ornare magna eros, eu pellentesque tortor vestibulum ut.


Collaborators: Arista Jusuf and Joy Ortiz
Historically, Silesia was a region that spanned across nations, carrying with it a rich tradition of handicraft and building. This creative identity has been lost due to a long history of European conflict. The Silesian Museum is the only repository of that cultural past, though the local pride for this history is still present in today’s contemporary furniture industry.
Our proposal is to revitalize the art of handicraft. Bzionkow will become a satellite of the Silesian Museum, designed for experimentation and exploration of this creative history. To connect Bzionkow back to its historical international context, Wroclaw – the new cultural capital of the European Union in 2016 – will become a launching point for the site’s inauguration.
Bzionkow’s buildings hold a richness expressed in their materials and construction. Our interventions and renovations will empathize with the site by reflecting old structures within their new counterparts. A series of phases will transform the site’s temporary role as a branch of Wroclaw 2016 into a center for culture and craft connected the Silesian Museum. Bzionkow will then become a place where past and present ideas of “handicraft” can be discussed through new works of art.
Our proposal is to revitalize the art of handicraft by transforming Bzionkow into a center for exploring craft and bringing back the craft culture that was once the pride of Silesia.
The European Union makes sure to acknowledge Europe not as nations with borders, but as a series of nodes, all of which have something unique to value. Our site is located in the region of Silesia, an area that is not defined by national borders and holds a history of craft that has now been lost to history.
Today, the region still specializes in furniture and takes pride in it even if it is only machine craft. Our goal is to take this pride and propel it forward, providing a space for craft to be rediscovered and Silesian pride to be harbored.
To achieve this goal we will connect Bzionkow to pivotal groups in the short term and in the long term. Bzionkow will serve as a satellite for Wroclaw, the European Capital of Culture for 2016 and will connect to the Silesian Museum to serve in the way that MoMA is a place to exhibit art and MoMA PS1 serves as an exploratory venue for artists.
Bzionkow, Our site is comparable in scale to Cornell’s Arts Quad or even the piazza at the vatican. This means that it can have immense influence if we let it.
It’s composed of almost a dozen buildings in different states of disrepair, each of which tells you about the site’s story and reveals how deeply ingrained in history Bzionkow is.
The estate grew and shrank over time, directly affected by important events in history and is strongly affected by the changes in national borders it experienced.
It’s our belief that the buildings of our site reflect this history and this richness in their textures, in the craft that created them.
We analyzed the varying states of disrepair of the buildings and concluded that only some of them were immediately habitable.
The floor areas and the ways the rooms area already arranged gave us clues to how much and how quickly the site can begin to accommodate visitors.
The project will take place in a series of phases. Wroclaw 2016 is an immediate event that will activate the site immediately and it will then be built upon to accommodate for more people as Bzionkow integrates itself more as a satellite to the Silesian Museum and generates its own identity.
We will be creating an immediate structure to be built quickly and efficiently and be ready soon. The surrounding buildings will not just be exhibition spaces, they will be exhibitions themselves. As the phases continue the surrounding buildings will be slowly restored to working order and used to house people, give them spaces to work, cafes, etc. slowly making the transition from old and programless to cherished and full of acivity while our original building grows sparser and emptier, effectively switching the roles of the new and the old buildings.
We have analyzed the existing buildings to take advantage of their structural stability and cherish their historical texture.
Renovations will reflect the original forms and structures and mend the past and present.
Phase 1
Phase 2
Phase 3
Web Address
Mailing Address
4705 W Le Moyne St
Chicago, IL 60651


URL is required URL must conform to URL format http[s]://...
Title is required
Tag List is required Tags must be separated with a comma, ex: foo,bar,goo


{% extends "base.html" %} {% load crispy_forms_tags %} {% load static %} {% block content %}
We Hope you enjoyed your experience and hope to see you soon.
Would you like to log back in?
Login


I LOVE TROUBLE A film review by Jon Ridge Copyright 1994 Jon Ridge
CAST: Julia Roberts, Nick Nolte, Saul Rubinek, James Rebhorn, Robert Loggia DIRECTOR: Charles Shyer SCREENPLAY: Nancy Meyers and Charles Shyer CINEMATOGRAPHY: John Lindley RUNNING TIME: 2:01 RELEASE: June 29, 1994
Julia Roberts walks into this film like a dream. Dressed in suit and skirt, her long legs and hips moving in perfect rhythm with a confident stride, she strolls smoothly through the cite of a train wreck, sparks a-flying, and into the life of rival reporter Peter Beckett (Nick Nolte). She's just what he envisions in a woman--beautiful, sexy and, more importantly, insecure enough to know less about what she does for a living than him. It's a tidy, engaging introduction to a movie that, unfortunately for these two talented stars, has no involving story to tell.
Writers Nancy Meyers and Charles Shyer have given Roberts a character she can really sink her teeth into. She plays Sabrina Peterson, a cub reporter for the Chicago Globe, whose only apparent goal in life is to out-scoop the famous Peter Brackett. Perhaps it's a way of getting ahead in her own publishing firm, getting a reputation, or proving her independence--that she isn't just a pretty face on the job--that gives her such ravenous interest in a case involving some sort of hormone designed to make cows produce milk earlier than they need to. I LOVE TROUBLE isn't really about the investigation these columnists pursue--and shouldn't treat it with the importance this film does--but a subtle, light romantic comedy about two people who would seem to have absolutely nothing in common but the work and wind up more intimately involved than expected. The dialogue given them is sporadically snappy banter, and Roberts and Nolte breeze through it with the smiles and batting eyes of two veterans. What they do not need is a moronic, recycled subplot with murderers that will put them in danger at the film's apex. And yet, I LOVE TROUBLE is another in the long, long, long line of movies to emerge from Hollywood in recent years featuring potentially talented writers who naturally assume (based on what they've seen before them) they must give an audience what the industry can't seem to do without.
The clash between comic duo and suspense subtext couldn't work less than it does here. The continuous report being executed is uninteresting; the villains are helplessly un-written; the peril--including an elevator shaft and unsteady platforms--is boring. But all the while there is Julia Roberts (who looks great in a knit sweater and jeans). Having returned to the screen after two hectic years of personal unease, Roberts seems to have found an understanding of herself, and what it is that makes her a charismatic persona. Director Charles Shyer definitely knows what it is, and captures it in the best part of his picture: the grin, the eyes, the legs. We get a lot of it, as Nolte gazes at her in the beginning and never seems to take his eyes off her; a scene in which he peeps through a keyhole at Roberts' slender legs lets you know exactly what his character thinks of her own, and what we should all concentrate on more than anything. Even during PRETTY WOMAN and FLATLINERS, I can't remember ever enjoying watching Roberts talk in a movie more.
Nolte is his suave self, but he too cannot escape the irreparable doom this film has made for itself. It's completely predictable fluff, with mild comic touches here and there and barely a thing to remember it by. Julia Roberts is beautiful to look at, but that alone does not a movie make.
Rated PG CRITICAL RATING: ** (1/2)
.
The review above was posted to the
rec.arts.movies.reviews newsgroup (de.rec.film.kritiken for German reviews).
The Internet Movie Database accepts no responsibility for the contents of the
review and has no editorial control. Unless stated otherwise, the copyright
belongs to the author.
Please direct comments/criticisms of the review to relevant newsgroups.
Broken URLs inthe reviews are the responsibility of the author.
The formatting of the review is likely to differ from the original due
to ASCII to HTML conversion.
Related links: index of all rec.arts.movies.reviews reviews


We manage inactive taxis for car owners. Whether you need to go on vacation or have some other reason for not driving your car, you don't have to worry about it being a liability anymore. As long as you have your car, it can earn you money.
We rent taxi-cabs to licensed drivers that need a car to drive. Stop letting your Hack license go to waste. Not having a car is no longer a reason to not make money. We can help you get into a street hail livery or Uber car today.
Green Livery started out as a simple idea. The CEO Sergio Sanchez began Green Livery as an experiment managing taxis for a couple of friends. They were so impressed with Sergio's work that they encouraged him to officially start the business and became Green Livery's very first investors!
Green Livery official set up its headquarters in the Bronx, NY and hit the streets to find it's very first clients! From a few clients to dozens, our awesome company just keeps growing!
To keep up with Green Livery's excelerating growth, CEO Sanchez declares a company move to Astoria Queens, the heart of the taxi industry!
With a great team and the best clients, we're ready for additional investors and the next phase of our growth!
Founder and CEO
Head of Finance
Lead Developer
The Green Livery team has been together during the tough times and the good times. Each of us is an expert in our field, contributing to Green Livery's evolution and growth in a unique way.


Analysis occurs only when the domain expert is in the room (otherwise it is pseudo-analysis) --Brad Kain, quoted in "UML Distilled"